equal
deleted
inserted
replaced
200 BP "name" "lam" ("_ ::= _" [100,100] 100) |
200 BP "name" "lam" ("_ ::= _" [100,100] 100) |
201 binder |
201 binder |
202 bi::"bp \<Rightarrow> name set" |
202 bi::"bp \<Rightarrow> name set" |
203 where |
203 where |
204 "bi (BP x t) = {x}" |
204 "bi (BP x t) = {x}" |
205 |
205 print_theorems |
206 |
206 |
207 text {* examples 2 *} |
207 text {* examples 2 *} |
208 nominal_datatype trm = |
208 nominal_datatype trm = |
209 Var "string" |
209 Var "name" |
210 | App "trm" "trm" |
210 | App "trm" "trm" |
211 | Lam x::"name" t::"trm" bindset x in t |
211 | Lam x::"name" t::"trm" bindset x in t |
212 | Let p::"pat" "trm" t::"trm" bind "f p" in t |
212 | Let p::"pat" "trm" t::"trm" bind "f p" in t |
213 and pat = |
213 and pat = |
214 PN |
214 PN |
220 "f PN = {}" |
220 "f PN = {}" |
221 | "f (PS x) = {x}" |
221 | "f (PS x) = {x}" |
222 | "f (PD (x,y)) = {x,y}" |
222 | "f (PD (x,y)) = {x,y}" |
223 |
223 |
224 nominal_datatype trm2 = |
224 nominal_datatype trm2 = |
225 Var2 "string" |
225 Var2 "name" |
226 | App2 "trm2" "trm2" |
226 | App2 "trm2" "trm2" |
227 | Lam2 x::"name" t::"trm2" bindset x in t |
227 | Lam2 x::"name" t::"trm2" bindset x in t |
228 | Let2 p::"pat2" "trm2" t::"trm2" bind "f2 p" in t |
228 | Let2 p::"pat2" "trm2" t::"trm2" bind "f2 p" in t |
229 and pat2 = |
229 and pat2 = |
230 PN2 |
230 PN2 |