equal
deleted
inserted
replaced
9 |
9 |
10 theory Pattern_Nits |
10 theory Pattern_Nits |
11 imports Main |
11 imports Main |
12 begin |
12 begin |
13 |
13 |
14 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s, |
14 nitpick_params [card = 10, max_potential = 0, sat_solver = MiniSat_JNI, |
15 card = 14] |
15 max_threads = 1, timeout = 60 s] |
16 |
16 |
17 lemma "x = (case u of () \<Rightarrow> y)" |
17 lemma "x = (case u of () \<Rightarrow> y)" |
18 nitpick [expect = genuine] |
18 nitpick [expect = genuine] |
19 oops |
19 oops |
20 |
20 |
130 |
130 |
131 lemma "\<exists>y ys. xs = y # ys" |
131 lemma "\<exists>y ys. xs = y # ys" |
132 nitpick [expect = genuine] |
132 nitpick [expect = genuine] |
133 oops |
133 oops |
134 |
134 |
135 lemma "\<exists>y a b zs. x = (y # Some (a, b) # zs)" |
135 lemma "\<exists>y a b zs. x = y # Some (a, b) # zs" |
136 nitpick [expect = genuine] |
136 nitpick [expect = genuine] |
137 oops |
137 oops |
138 |
138 |
139 end |
139 end |