 08 Feb, 2018 1 commit


Robbert Krebbers authored
`NoBackTrack P` requires `P` but will never backtrack on it once a result for `P` has been found.

 02 Feb, 2018 1 commit


Robbert Krebbers authored

 31 Jan, 2018 5 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 14 Jan, 2018 1 commit


Robbert Krebbers authored
This is needed so that it can be used be used as a combinator for defining induction schemes for mutually inductive types.

 12 Jan, 2018 1 commit


Robbert Krebbers authored

 10 Jan, 2018 1 commit


Robbert Krebbers authored
As we have for all classes for binary relations.

 08 Dec, 2017 1 commit


Robbert Krebbers authored

 05 Dec, 2017 1 commit


Ralf Jung authored

 04 Dec, 2017 2 commits


JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

 29 Nov, 2017 2 commits


Robbert Krebbers authored

David Swasey authored
Enable one to import both stdpp's base and ssrfun. Note that (f x.1) now parses as (f (fst x)) rather than (fst (f x)). (This change affects one proof in Iris.)

 21 Nov, 2017 1 commit


Robbert Krebbers authored
This gets rid of the old hack to have specific notations for pairs up to a fixed arity, and moreover allows to do fancy things like: ``` Record test := Test { t1 : nat; t2 : nat }. Definition foo (x : option test) : option nat := ''(Test a1 a2) ← x; Some a1. ```

 20 Nov, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
This one works for setoid rewriting under binders.

 18 Nov, 2017 1 commit


Ralf Jung authored

 16 Nov, 2017 2 commits
 12 Nov, 2017 2 commits


Robbert Krebbers authored
 Name all variables that we refer to.  Put types in definitions.

Robbert Krebbers authored
This follows the associativity in Haskell. So, something like f <$> g <$> h Is now parsed as: (f <$> g) <$> h Since the functor is a generalized form of function application, this also now also corresponds with the associativity of function application, which is also left associative.

 11 Nov, 2017 1 commit


Robbert Krebbers authored
This is similar to `f_equal/=`.

 09 Nov, 2017 6 commits


Johannes Kloos authored

Johannes Kloos authored

Johannes Kloos authored

Johannes Kloos authored

Robbert Krebbers authored

Robbert Krebbers authored

 01 Nov, 2017 9 commits


Johannes Kloos authored

Johannes Kloos authored

Johannes Kloos authored
Also make the instances nonglobal, to prevent multiple instance problems.

Johannes Kloos authored

Johannes Kloos authored

Johannes Kloos authored
We prove that various types are infinite, notably:  nat, N, positive and Z;  string (using prettyprinting of nat);  option, with an infinite element type;  list, with an inhabited element type. Furthermore, we instantiate Fresh for strings.

Johannes Kloos authored
This implements a simple linear search for fresh elements.

Johannes Kloos authored
This generalizes Fix_unfold to a setoid setting. In particular, we can use this to unfold multiargument fixpoints without requiring functional extensionality.

Johannes Kloos authored
Infinity is described by having an injection from nat.
