src/HOL/Quickcheck_Narrowing.thy
changeset 48565 7c497a239007
parent 48253 4410a709913c
child 48891 c0eafbd55de3
equal deleted inserted replaced
48561:12aa0cb2b447 48565:7c497a239007
   163 
   163 
   164 setup {* fold (Numeral.add_code @{const_name Num}
   164 setup {* fold (Numeral.add_code @{const_name Num}
   165   false Code_Printer.literal_numeral) ["Haskell_Quickcheck"]  *}
   165   false Code_Printer.literal_numeral) ["Haskell_Quickcheck"]  *}
   166 
   166 
   167 code_type code_int
   167 code_type code_int
   168   (Haskell_Quickcheck "Int")
   168   (Haskell_Quickcheck "Prelude.Int")
   169 
   169 
   170 code_const "0 \<Colon> code_int"
   170 code_const "0 \<Colon> code_int"
   171   (Haskell_Quickcheck "0")
   171   (Haskell_Quickcheck "0")
   172 
   172 
   173 code_const "1 \<Colon> code_int"
   173 code_const "1 \<Colon> code_int"
   220 
   220 
   221 code_const error (Haskell_Quickcheck "error")
   221 code_const error (Haskell_Quickcheck "error")
   222 
   222 
   223 consts toEnum :: "code_int => char"
   223 consts toEnum :: "code_int => char"
   224 
   224 
   225 code_const toEnum (Haskell_Quickcheck "toEnum")
   225 code_const toEnum (Haskell_Quickcheck "Prelude.toEnum")
   226 
   226 
   227 consts marker :: "char"
   227 consts marker :: "char"
   228 
   228 
   229 code_const marker (Haskell_Quickcheck "''\\0'")
   229 code_const marker (Haskell_Quickcheck "''\\0'")
   230 
   230