theory TypeVarsTestimports "../Nominal2" begin(* a nominal datatype with type variables and sorts *)(* the sort constraints need to be attached to the *)(* first occurence of the type variables on the *)(* right-hand side *)atom_decl nameclass s1class s2instance nat :: s1 ..instance int :: s2 .. nominal_datatype ('a::s1, 'b::s2, 'c::at) lam = Var "name"| App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"| Lam x::"name" l::"('a, 'b, 'c) lam" binds x in l| Foo "'a" "'b"| Bar x::"'c" l::"('a, 'b, 'c) lam" binds x in l (* Bar binds a polymorphic atom *)term Footerm Barthm lam.distinctthm lam.inductthm lam.exhaust thm lam.strong_exhaustthm lam.fv_defsthm lam.bn_defsthm lam.perm_simpsthm lam.eq_iffthm lam.fv_bn_eqvtthm lam.size_eqvtnominal_datatype ('alpha, 'beta, 'gamma) psi = PsiNil| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" nominal_datatype 'a foo = Node x::"name" f::"'a foo" binds x in f| Leaf "'a"term "Leaf"end