theory TypeVarsTest+
−
imports "../Nominal2" +
−
begin+
−
+
−
atom_decl name+
−
declare [[STEPS = 100]]+
−
+
−
class s1+
−
class s2+
−
+
−
nominal_datatype ('a, 'b) lam =+
−
  Var "name"+
−
| App "('a::s1, 'b::s2) lam" "('a, 'b) lam"+
−
| Lam x::"name" l::"('a, 'b) lam"  bind x in l+
−
+
−
thm lam.distinct+
−
thm lam.induct+
−
thm lam.exhaust+
−
thm lam.fv_defs+
−
thm lam.bn_defs+
−
thm lam.perm_simps+
−
thm lam.eq_iff+
−
thm lam.fv_bn_eqvt+
−
thm lam.size_eqvt+
−
+
−
+
−
end+
−
+
−
+
−
+
−