equal
deleted
inserted
replaced
5 text {* example 1 *} |
5 text {* example 1 *} |
6 |
6 |
7 nominal_datatype lam = |
7 nominal_datatype lam = |
8 VAR "name" |
8 VAR "name" |
9 | APP "lam" "lam" |
9 | APP "lam" "lam" |
10 | LET bp::"bp" t::"lam" bind "bi bp" in t ("Let _ in _" [100,100] 100) |
10 | LET bp::"bp" t::"lam" bind "bi bp" in t |
11 and bp = |
11 and bp = |
12 BP "name" "lam" ("_ ::= _" [100,100] 100) |
12 BP "name" "lam" |
13 binder |
13 binder |
14 bi::"bp \<Rightarrow> name set" |
14 bi::"bp \<Rightarrow> name set" |
15 where |
15 where |
16 "bi (BP x t) = {x}" |
16 "bi (BP x t) = {x}" |
17 |
17 |