GitLab

typeclass comments

See merge request robbertkrebbers/coq-stdpp!24

Lattices notation for order, join, meet, top and bot.

See merge request robbertkrebbers/coq-stdpp!23

Make x.1, x.2 notation compatible with ssrfun.

See merge request robbertkrebbers/coq-stdpp!21

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.)

Allow compiling against "dev" version of Coq

See merge request robbertkrebbers/coq-stdpp!20

This matches e.g. Iris allowing a "dev" version of std++: You can install a
"dev" version to test stuff, but then you are responsible for making sure that
these versions actually work together.  We rely on that when testing things
against Iris master every night, for which purpose we install Iris master as
"dev" version.

Pattern matching notation for monadic binds

See merge request robbertkrebbers/coq-stdpp!18

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.
```

This one works for setoid rewriting under binders.

Factor out solve_proper_prepare

See merge request robbertkrebbers/coq-stdpp!19

- Name all variables that we refer to.
- Put types in definitions.

Provide an Infinite typeclass and a generic implementation of Fresh.

See merge request robbertkrebbers/coq-stdpp!13

Make `fmap` left associative.

See merge request robbertkrebbers/coq-stdpp!16

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.

This is similar to `f_equal/=`.

Use `stdpp_scope` for all notations.

See merge request robbertkrebbers/coq-stdpp!17

Also make the instances non-global, to prevent multiple instance
problems.

We prove that various types are infinite, notably:
- nat, N, positive and Z;
- string (using pretty-printing of nat);
- option, with an infinite element type;
- list, with an inhabited element type.

Furthermore, we instantiate Fresh for strings.

This implements a simple linear search for fresh elements.