Don't need type signature for sub

Changes

1 changed files (+4/-4)

• lambcalc.lean
  • @@ -9,10 +9,10 @@ inductive Term where
    def red : Term → Term | .A fn arg => match red fn with - | .L body => let rec sub : Nat → Term → Term - | 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' + | .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' sub 0 body | other => .A other arg | other => other