theory TestMorePerm
imports "../NewParser"
begin

text {* 
  "Weirdo" example from Peter Sewell's bestiary. 

  This example is not covered by our binding 
  specification.

*}
ML {* val _ = cheat_equivp := true *}

atom_decl name

nominal_datatype weird =
  Foo_var "name"
| Foo_pair "weird" "weird" 
| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
    bind x in p1 p2, 
    bind y in p2 p3

thm alpha_weird_raw.intros[no_vars]

thm permute_weird_raw.simps[no_vars]
thm alpha_weird_raw.intros[no_vars]
thm fv_weird_raw.simps[no_vars]

declare permute_weird_raw.simps[eqvt]
declare alpha_gen_eqvt[eqvt]
equivariance alpha_weird_raw


end