theory NoneExamplesimports "../NewParser"beginatom_decl name(* this example binds bound names and so is not respectful *)(*nominal_datatype trm = Vr "name"| Lm x::"name" t::"trm" bind x in t| Lt left::"trm" right::"trm" bind "bv left" in rightbinder bvwhere "bv (Vr n) = {}"| "bv (Lm n t) = {atom n} \<union> bv t"| "bv (Lt l r) = bv l \<union> bv r"*)(* this example uses "-" in the binding function; at the moment this is unsupported *)(*nominal_datatype trm' = Vr' "name"| Lm' l::"name" r::"trm'" bind l in r| Lt' l::"trm'" r::"trm'" bind "bv' l" in rbinder bv'where "bv' (Vr' n) = {atom n}"| "bv' (Lm' n t) = bv' t - {atom n}"| "bv' (Lt' l r) = bv' l \<union> bv' r"*)(* this example again binds bound names *)(*nominal_datatype trm'' = Va'' "name"| Lm'' n::"name" l::"trm''" bind n in land bla'' = Bla'' f::"trm''" s::"trm''" bind "bv'' f" in sbinder bv''where "bv'' (Vm'' x) = {}"| "bv'' (Lm'' x b) = {atom x}"*)end