spl / alpha-conversion-is-easy

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

Do all update/lam functions fit the same pattern? #38

Open spl opened 6 years ago

spl commented 6 years ago

The possible pattern:

if p : _ = _ then _ else _ p

Should we lift this pattern to a common update def to make this clear? Or would that obscure it more?