equal
deleted
inserted
replaced
37 in |
37 in |
38 Numeral.add_code \<^const_name>\<open>Code_Numeral.Pos\<close> I print target |
38 Numeral.add_code \<^const_name>\<open>Code_Numeral.Pos\<close> I print target |
39 #> Numeral.add_code \<^const_name>\<open>Code_Numeral.Neg\<close> (~) print target |
39 #> Numeral.add_code \<^const_name>\<open>Code_Numeral.Neg\<close> (~) print target |
40 end |
40 end |
41 \<close> |
41 \<close> |
|
42 |
|
43 code_printing |
|
44 constant Code_Numeral.push_bit \<rightharpoonup> |
|
45 (Haskell_Quickcheck) "Bit'_Shifts.drop'" |
|
46 | constant Code_Numeral.drop_bit \<rightharpoonup> |
|
47 (Haskell_Quickcheck) "Bit'_Shifts.push'" |
42 |
48 |
43 |
49 |
44 subsubsection \<open>Narrowing's deep representation of types and terms\<close> |
50 subsubsection \<open>Narrowing's deep representation of types and terms\<close> |
45 |
51 |
46 datatype (plugins only: code extraction) narrowing_type = |
52 datatype (plugins only: code extraction) narrowing_type = |