equal
deleted
inserted
replaced
1 (* Author: Pascal Stoop, ETH Zurich |
1 (* Author: Pascal Stoop, ETH Zurich |
2 Author: Andreas Lochbihler, Digital Asset *) |
2 Author: Andreas Lochbihler, Digital Asset *) |
|
3 |
|
4 section \<open>Eliminating pattern matches\<close> |
3 |
5 |
4 theory Case_Converter |
6 theory Case_Converter |
5 imports Main |
7 imports Main |
6 begin |
8 begin |
7 |
|
8 subsection \<open>Eliminating pattern matches\<close> |
|
9 |
9 |
10 definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where |
10 definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where |
11 [code del]: "missing_pattern_match m f = f ()" |
11 [code del]: "missing_pattern_match m f = f ()" |
12 |
12 |
13 lemma missing_pattern_match_cong [cong]: |
13 lemma missing_pattern_match_cong [cong]: |