• Robbert Krebbers's avatar
    Change notations of big_ops for upred. · 93792f5c
    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 Loading commit data...
environments.v Loading commit data...
ghost_ownership.v Loading commit data...
intro_patterns.v Loading commit data...
invariants.v Loading commit data...
notation.v Loading commit data...
pviewshifts.v Loading commit data...
spec_patterns.v Loading commit data...
sts.v Loading commit data...
tactics.v Loading commit data...
weakestpre.v Loading commit data...