Re: [isabelle] Non-exhaustive case certificates



I forgot:

lemma new_foo_case_cert:
assumes "CASE == foo_case a b c d"
shows "(CASE A == a) &&& (CASE B == b) &&& (CASE C == c)"
using assms by auto
setup {*
Code.add_case @{thm new_foo_case_cert}
*}

Case certificates must always be exhaustive!

	Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.