5 text {* weirdo example from Peter Sewell's bestiary *}

     5 text {* 

     6   "Weirdo" example from Peter Sewell's bestiary. 

     7 nominal_datatype weird =

     8   In case of deep binders, it is not coverd by our 

     8   WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"

     9   approach of defining alpha-equivalence with a 

     9     bind x in p1, bind x in p2, bind y in p2, bind y in p3

    10   single permutation.

    10 | WV "name"

    11 

    11 | WP "weird" "weird"

    12   Check whether it works with shallow binders as

    13   defined below.

    14 

    15 *}

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

    17 

    18 atom_decl name

    19 

    20 nominal_datatype foo =

    21   Foo_var "name"

    22 | Foo_pair "foo" "foo" 

    23 | Foo x::"name" y::"name" p1::"foo" p2::"foo" p3::"foo"

    24     bind x in p1, bind x in p2, 

    25     bind y in p2, bind y in p3

    26 

    27 thm alpha_foo_raw.intros[no_vars]