equal
deleted
inserted
replaced
896 qed |
896 qed |
897 |
897 |
898 |
898 |
899 subsection {* Code generation for div, mod and dvd on nat *} |
899 subsection {* Code generation for div, mod and dvd on nat *} |
900 |
900 |
901 definition [code nofunc]: |
901 definition [code func del]: |
902 "divmod (m\<Colon>nat) n = (m div n, m mod n)" |
902 "divmod (m\<Colon>nat) n = (m div n, m mod n)" |
903 |
903 |
904 lemma divmod_zero [code]: "divmod m 0 = (0, m)" |
904 lemma divmod_zero [code]: "divmod m 0 = (0, m)" |
905 unfolding divmod_def by simp |
905 unfolding divmod_def by simp |
906 |
906 |