equal
deleted
inserted
replaced
113 |
113 |
114 definition add_raw where |
114 definition add_raw where |
115 "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))" |
115 "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))" |
116 |
116 |
117 quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw |
117 quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw |
|
118 unfolding add_raw_def by auto |
118 |
119 |
119 lemma "add x y = add x x" |
120 lemma "add x y = add x x" |
120 nitpick [show_datatypes, expect = genuine] |
121 nitpick [show_datatypes, expect = genuine] |
121 oops |
122 oops |
122 |
123 |