-
Robbert Krebbers authored
Rationale: to make the code closer to what is on paper, I want the notations to look like quantifiers, i.e. have a binder built-in. I thus introduced the following notations: [★ map] k ↦ x ∈ m, P [★ set] x ∈ X, P The good thing - contrary to the notations that we had before that required an explicit lambda - is that type annotations of k and x are now not printed making goals much easier to read.
93792f5c
Name |
Last commit
|
Last update |
---|---|---|
.. | ||
coq_tactics.v | ||
environments.v | ||
ghost_ownership.v | ||
intro_patterns.v | ||
invariants.v | ||
notation.v | ||
pviewshifts.v | ||
spec_patterns.v | ||
sts.v | ||
tactics.v | ||
weakestpre.v |