theory Test
imports "../NewParser"
begin

declare [[STEPS = 4]]

atom_decl name

(*
nominal_datatype trm =
  Vr "name"
| Ap "trm" "trm"

thm fv_trm_raw.simps[no_vars]
*)

(* This file contains only the examples that are not supposed to work yet. *)


declare [[STEPS = 2]]


(* 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 trm =
  Vr "name"
| Ap "trm" "trm list"
| Lm x::"name" t::"trm"  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]
*)

end