6 

     7 

     8 text {* 

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

    10 

    11   This example is not covered by our binding 

    12   specification.

    13 

    14 *}

    15 

    16 nominal_datatype weird =

    17   Foo_var "name"

    18 | Foo_pair "weird" "weird" 

    19 | Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"

    20     bind x in p1 p2, 

    21     bind y in p2 p3

    22 

    23 (* e1 occurs in two bodies *)

    24 

    25 nominal_datatype exp =

    26   Var name

    27 | Pair exp exp

    28 | LetRec x::name p::pat e1::exp e2::exp  bind x in e1 e2, bind "bp p" in e1

    29 and pat =

    30   PVar name

    31 | PUnit

    32 | PPair pat pat

    33 binder

    34   bp :: "pat \<Rightarrow> atom list"

    35 where

    36   "bp (PVar x) = [atom x]"

    37 | "bp (PUnit) = []"

    38 | "bp (PPair p1 p2) = bp p1 @ bp p2"

    39