equal
deleted
inserted
replaced
11 A simple example on quote / antiquote in higher-order abstract |
11 A simple example on quote / antiquote in higher-order abstract |
12 syntax. |
12 syntax. |
13 *} |
13 *} |
14 |
14 |
15 syntax |
15 syntax |
16 "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999) |
16 "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999) |
17 |
17 |
18 constdefs |
18 constdefs |
19 var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999) |
19 var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999) |
20 "var x env == env x" |
20 "var x env == env x" |
21 |
21 |
22 Expr :: "(('a => nat) => nat) => ('a => nat) => nat" |
22 Expr :: "(('a => nat) => nat) => ('a => nat) => nat" |
23 "Expr exp env == exp env" |
23 "Expr exp env == exp env" |
24 |
24 |
27 |
27 |
28 term "EXPR (a + b + c)" |
28 term "EXPR (a + b + c)" |
29 term "EXPR (a + b + c + VAR x + VAR y + 1)" |
29 term "EXPR (a + b + c + VAR x + VAR y + 1)" |
30 term "EXPR (VAR (f w) + VAR x)" |
30 term "EXPR (VAR (f w) + VAR x)" |
31 |
31 |
32 term "Expr (\<lambda>env. env x)" (*improper*) |
32 term "Expr (\<lambda>env. env x)" -- {* improper *} |
33 term "Expr (\<lambda>env. f env)" |
33 term "Expr (\<lambda>env. f env)" |
34 term "Expr (\<lambda>env. f env + env x)" (*improper*) |
34 term "Expr (\<lambda>env. f env + env x)" -- {* improper *} |
35 term "Expr (\<lambda>env. f env y z)" |
35 term "Expr (\<lambda>env. f env y z)" |
36 term "Expr (\<lambda>env. f env + g y env)" |
36 term "Expr (\<lambda>env. f env + g y env)" |
37 term "Expr (\<lambda>env. f env + g env y + h a env z)" |
37 term "Expr (\<lambda>env. f env + g env y + h a env z)" |
38 |
38 |
39 end |
39 end |