• 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
upred_big_op.v 12.1 KB