equal
deleted
inserted
replaced
6 imports "../Nominal" |
6 imports "../Nominal" |
7 begin |
7 begin |
8 |
8 |
9 atom_decl name |
9 atom_decl name |
10 |
10 |
11 nominal_datatype lam = Var "name" |
11 nominal_datatype lam = |
12 | App "lam" "lam" |
12 Var "name" |
13 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
13 | App "lam" "lam" |
|
14 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
14 |
15 |
15 text {* definition of the height-function on lambda-terms *} |
16 text {* definition of the height-function on lambda-terms *} |
16 |
17 |
17 consts |
18 consts |
18 height :: "lam \<Rightarrow> int" |
19 height :: "lam \<Rightarrow> int" |