6 declare [[STEPS = 100]]

     6 declare [[STEPS = 100]]

     7 

     7 

     8 class s1

     8 class s1

     9 class s2

     9 class s2

    10 

    10 

    11 nominal_datatype ('a, 'b) lam =

    12 nominal_datatype ('a, 'b) lam =

    12   Var "name"

    13   Var "name"

    13 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam"

    14 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam"

    14 | Lam x::"name" l::"('a, 'b) lam"  bind x in l

    15 | Lam x::"name" l::"('a, 'b) lam"  bind x in l

    15 

    16 

    20 thm lam.bn_defs

    21 thm lam.bn_defs

    21 thm lam.perm_simps

    22 thm lam.perm_simps

    22 thm lam.eq_iff

    23 thm lam.eq_iff

    23 thm lam.fv_bn_eqvt

    24 thm lam.fv_bn_eqvt

    24 thm lam.size_eqvt

    25 thm lam.size_eqvt

    26 

    27 

    27 end

    28 end

    28 

    29 

    29 

    30 

    30 

    31