search

spl / alpha-conversion-is-easy

Lean proof of alpha-conversion is easy
4 stars 0 forks source link

Use same pair notation in vrel and vrel.update #29

Open spl opened 6 years ago

spl commented 6 years ago

Currently:

notation `⟪` x `, ` y `⟫` ` ∈ν ` R:50 := R x y
notation R ` ⩁ `:65 (a `, ` b) := vrel.update a b R