src/HOL/Quickcheck_Narrowing.thy
changeset 58400 d0d3c30806b4
parent 58350 919149921e46
child 58813 625d04d4fd2a
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Sep 18 18:48:04 2014 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Sep 18 18:48:54 2014 +0200
     1.3 @@ -23,6 +23,20 @@
     1.4  
     1.5  code_reserved Haskell_Quickcheck Typerep
     1.6  
     1.7 +code_printing
     1.8 +  constant "0::integer" \<rightharpoonup>
     1.9 +    (Haskell_Quickcheck) "!(0/ ::/ Prelude.Int)"
    1.10 +
    1.11 +setup {*
    1.12 +  let
    1.13 +    val target = "Haskell_Quickcheck";
    1.14 +    fun print _ = Code_Haskell.print_numeral "Prelude.Int";
    1.15 +  in
    1.16 +    Numeral.add_code @{const_name Code_Numeral.Pos} I print target
    1.17 +    #> Numeral.add_code @{const_name Code_Numeral.Neg} (op ~) print target
    1.18 +  end
    1.19 +*}
    1.20 +
    1.21  
    1.22  subsubsection {* Narrowing's deep representation of types and terms *}
    1.23