theory Test+ −
imports "../Parser"+ −
begin+ −
+ −
(* This file contains only the examples that are not supposed to work yet. *)+ −
+ −
+ −
atom_decl name+ −
+ −
(* example 4 from Terms.thy *)+ −
(* fv_eqvt does not work, we need to repaire defined permute functions+ −
defined fv and defined alpha... *)+ −
(* lists-datastructure does not work yet+ −
nominal_datatype trm4 =+ −
Vr4 "name"+ −
| Ap4 "trm4" "trm4 list"+ −
| Lm4 x::"name" t::"trm4" bind x in t+ −
+ −
thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]+ −
thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]+ −
*)+ −
+ −
(* example 8 from Terms.thy *)+ −
+ −
(* Binding in a term under a bn, needs to fail *)+ −
(*+ −
nominal_datatype foo8 =+ −
Foo0 "name"+ −
| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"+ −
and bar8 =+ −
Bar0 "name"+ −
| Bar1 "name" s::"name" b::"bar8" bind s in b+ −
binder+ −
bv8+ −
where+ −
"bv8 (Bar0 x) = {}"+ −
| "bv8 (Bar1 v x b) = {atom v}"+ −
*)+ −
+ −
end+ −
+ −
+ −