equal
deleted
inserted
replaced
5 |
5 |
6 atom_decl name |
6 atom_decl name |
7 |
7 |
8 nominal_datatype lt = |
8 nominal_datatype lt = |
9 Var name ("_~" [150] 149) |
9 Var name ("_~" [150] 149) |
|
10 | App lt lt (infixl "$" 100) |
10 | Lam x::"name" t::"lt" binds x in t |
11 | Lam x::"name" t::"lt" binds x in t |
11 | App lt lt (infixl "$" 100) |
|
12 |
12 |
13 nominal_primrec |
13 nominal_primrec |
14 subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt" ("_ [_ ::= _]" [90, 90, 90] 90) |
14 subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt" ("_ [_ ::= _]" [90, 90, 90] 90) |
15 where |
15 where |
16 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
16 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |