equal
deleted
inserted
replaced
30 setup \<open> |
30 setup \<open> |
31 let |
31 let |
32 val target = "Haskell_Quickcheck"; |
32 val target = "Haskell_Quickcheck"; |
33 fun print _ = Code_Haskell.print_numeral "Prelude.Int"; |
33 fun print _ = Code_Haskell.print_numeral "Prelude.Int"; |
34 in |
34 in |
35 Numeral.add_code @{const_name Code_Numeral.Pos} I print target |
35 Numeral.add_code \<^const_name>\<open>Code_Numeral.Pos\<close> I print target |
36 #> Numeral.add_code @{const_name Code_Numeral.Neg} (~) print target |
36 #> Numeral.add_code \<^const_name>\<open>Code_Numeral.Neg\<close> (~) print target |
37 end |
37 end |
38 \<close> |
38 \<close> |
39 |
39 |
40 |
40 |
41 subsubsection \<open>Narrowing's deep representation of types and terms\<close> |
41 subsubsection \<open>Narrowing's deep representation of types and terms\<close> |
52 |
52 |
53 primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons" |
53 primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons" |
54 where |
54 where |
55 "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (\<lambda>c. f \<circ> c) cs)" |
55 "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (\<lambda>c. f \<circ> c) cs)" |
56 |
56 |
57 subsubsection \<open>From narrowing's deep representation of terms to @{theory HOL.Code_Evaluation}'s terms\<close> |
57 subsubsection \<open>From narrowing's deep representation of terms to \<^theory>\<open>HOL.Code_Evaluation\<close>'s terms\<close> |
58 |
58 |
59 class partial_term_of = typerep + |
59 class partial_term_of = typerep + |
60 fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term" |
60 fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term" |
61 |
61 |
62 lemma partial_term_of_anything: "partial_term_of x nt \<equiv> t" |
62 lemma partial_term_of_anything: "partial_term_of x nt \<equiv> t" |