Make it pretty

Changes

1 changed files (+7/-7)

• lambcalc.lean
  • @@ -7,14 +7,14 @@ inductive Term where
    | V : Nat → Term def red : Term → Term - | Term.A fn arg => + | .A fn arg => match red fn with - | Term.L body => let rec sub : Nat → Term → Term - | n, (Term.A fn arg) => Term.A (sub n fn) (sub n arg) - | n, (Term.L body) => Term.L (sub (n + 1) body) - | n, (Term.V n') => if n == n' then arg else Term.V n' + | .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' sub 0 body - | other => Term.A other arg + | other => .A other arg | other => other - #eval red <| Term.A (Term.L (Term.V 69)) (Term.V 1) + #eval red <| .A (.L (.V 69)) (.V 1)