Jérémie Koenig
jeremie-koenig

Organizations

@CertiKOS
Aug 19, 2016
@jeremie-koenig
Aug 19, 2016
@jeremie-koenig
Need a good scheme for relator notations
Aug 19, 2016
@jeremie-koenig
Notations for Proper, Monotonic don't play well with scopes
Aug 19, 2016
@jeremie-koenig
  • @jeremie-koenig d202737
    Sort out the names of classes and relations
Aug 19, 2016
@jeremie-koenig
Figure out the `Related` vs. `Proper` vs. `Monotonic` vs. `MonotonicPair` nomenclature
Aug 19, 2016
@jeremie-koenig
Drop support for Coq 8.4
Aug 19, 2016
@jeremie-koenig
Investigate a leftward arrow
Aug 19, 2016
jeremie-koenig commented on issue CertiKOS/coqrel#4
@jeremie-koenig

Random thoughts/complement: forallp_rel (essentially Π _ | v1 v2 : E), could be Π v1 v2 : E, R[v1,v2]. Π v1 v2, R[v1, v2] could be a new relator…

Aug 19, 2016
@jeremie-koenig
Figure out the `Related` vs. `Proper` vs. `Monotonic` vs. `MonotonicPair` nomenclature
Aug 19, 2016
jeremie-koenig commented on issue CertiKOS/coqrel#4
@jeremie-koenig

A scheme along the following lines emerged from discussion with Matthieu Sozeau: for the Prop / logical case, use the rforall keyword (and/or ) a…

Aug 4, 2016
jeremie-koenig commented on issue CertiKOS/coqrel#5
@jeremie-koenig

Hi John, thanks for your interest in coqrel! We've decided to distribute the current prototype under an MIT license. We may end up choosing a diffe…

Aug 4, 2016
@jeremie-koenig
Jul 25, 2016
@jeremie-koenig
Need a good scheme for relator notations
Jul 25, 2016
@jeremie-koenig
Jul 3, 2016
@jeremie-koenig
Add backtracking to solve_monotonic
Jul 3, 2016
jeremie-koenig commented on issue CertiKOS/coqrel#2
@jeremie-koenig

Backtracking is now implemented in the rauto tactic. (As planned, I fixed Delay.v and used a typeclass reification of the components of the old sol…

Jul 3, 2016
@jeremie-koenig
Jun 17, 2016
@jeremie-koenig
Jun 11, 2016
@jeremie-koenig
Jun 8, 2016
@jeremie-koenig