theory Term8+ −
imports "../NewParser"+ −
begin+ −
+ −
(* example 8 *)+ −
+ −
atom_decl name+ −
+ −
(* this should work but gives an error at the moment:+ −
in alpha_bn_rsp proof.+ −
*)+ −
+ −
nominal_datatype foo =+ −
Foo0 "name"+ −
| Foo1 b::"bar" f::"foo" bind_set "bv b" in f+ −
and bar =+ −
Bar0 "name"+ −
| Bar1 "name" s::"name" b::"bar" bind_set s in b+ −
binder+ −
bv+ −
where+ −
"bv (Bar0 x) = {}"+ −
| "bv (Bar1 v x b) = {atom v}"+ −
+ −
+ −
end+ −
+ −
+ −