Changes
1 changed files (+2/-1)
-
-
@@ -9,7 +9,8 @@ inductive Term wheredef red : Term → Term | .A fn arg => match red fn with | .L body => let rec sub | .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'
-