equal
deleted
inserted
replaced
76 |
76 |
77 end |
77 end |
78 *} |
78 *} |
79 |
79 |
80 lemma [code]: |
80 lemma [code]: |
81 "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2 |
81 "HOL.equal (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> HOL.equal tyco1 tyco2 |
82 \<and> list_all2 eq_class.eq tys1 tys2" |
82 \<and> list_all2 HOL.equal tys1 tys2" |
83 by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric]) |
83 by (auto simp add: eq_equal [symmetric] list_all2_eq [symmetric]) |
|
84 |
|
85 lemma [code nbe]: |
|
86 "HOL.equal (x :: typerep) x \<longleftrightarrow> True" |
|
87 by (fact equal_refl) |
84 |
88 |
85 code_type typerep |
89 code_type typerep |
86 (Eval "Term.typ") |
90 (Eval "Term.typ") |
87 |
91 |
88 code_const Typerep |
92 code_const Typerep |