Theory HOL-Library.Case_Converter
section ‹Eliminating pattern matches›
theory Case_Converter
imports Main
begin
definition missing_pattern_match :: "String.literal ⇒ (unit ⇒ 'a) ⇒ 'a" where
[code del]: "missing_pattern_match m f = f ()"
lemma missing_pattern_match_cong [cong]:
"m = m' ⟹ missing_pattern_match m f = missing_pattern_match m' f"
by(rule arg_cong)
lemma missing_pattern_match_code [code_unfold]:
"missing_pattern_match = Code.abort"
unfolding missing_pattern_match_def Code.abort_def ..
ML_file ‹case_converter.ML›
end