equal
deleted
inserted
replaced
51 quickcheck[tester = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample] |
51 quickcheck[tester = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample] |
52 oops |
52 oops |
53 |
53 |
54 section {* Context Free Grammar *} |
54 section {* Context Free Grammar *} |
55 |
55 |
56 datatype_new alphabet = a | b |
56 datatype alphabet = a | b |
57 |
57 |
58 inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where |
58 inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where |
59 "[] \<in> S\<^sub>1" |
59 "[] \<in> S\<^sub>1" |
60 | "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1" |
60 | "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1" |
61 | "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1" |
61 | "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1" |
177 subsection {* IMP *} |
177 subsection {* IMP *} |
178 |
178 |
179 type_synonym var = nat |
179 type_synonym var = nat |
180 type_synonym state = "int list" |
180 type_synonym state = "int list" |
181 |
181 |
182 datatype_new com = |
182 datatype com = |
183 Skip | |
183 Skip | |
184 Ass var "int" | |
184 Ass var "int" | |
185 Seq com com | |
185 Seq com com | |
186 IF "state list" com com | |
186 IF "state list" com com | |
187 While "state list" com |
187 While "state list" com |
204 quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample] |
204 quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample] |
205 oops |
205 oops |
206 |
206 |
207 subsection {* Lambda *} |
207 subsection {* Lambda *} |
208 |
208 |
209 datatype_new type = |
209 datatype type = |
210 Atom nat |
210 Atom nat |
211 | Fun type type (infixr "\<Rightarrow>" 200) |
211 | Fun type type (infixr "\<Rightarrow>" 200) |
212 |
212 |
213 datatype_new dB = |
213 datatype dB = |
214 Var nat |
214 Var nat |
215 | App dB dB (infixl "\<degree>" 200) |
215 | App dB dB (infixl "\<degree>" 200) |
216 | Abs type dB |
216 | Abs type dB |
217 |
217 |
218 primrec |
218 primrec |