Oh oops it's = not ==

Changes

1 changed files (+1/-1)

• lambcalc.lean
  • @@ -12,7 +12,7 @@ def red : Term → Term
    | .L body => let rec sub | n, .A fn arg => .A (sub n fn) (sub n arg) | n, .L body => .L <| sub (n + 1) body - | n, .V n' => if n == n' then arg else .V n' + | n, .V n' => if n = n' then arg else .V n' sub 0 body | other => .A other arg | other => other