adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
authorbulwahn
Thu Jun 09 08:32:18 2011 +0200 (2011-06-09)
changeset 433127a31f9064f99
parent 43311 1efdcb579b6c
child 43313 d3c34987863b
adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
src/HOL/Quickcheck_Narrowing.thy
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:16 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:18 2011 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  header {* Counterexample generator preforming narrowing-based testing *}
     1.5  
     1.6  theory Quickcheck_Narrowing
     1.7 -imports Main "~~/src/HOL/Library/Code_Char"
     1.8 +imports Quickcheck_Exhaustive
     1.9  uses
    1.10    ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
    1.11    ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
    1.12 @@ -26,6 +26,20 @@
    1.13  
    1.14  code_reserved Haskell_Quickcheck Typerep
    1.15  
    1.16 +code_type char
    1.17 +  (Haskell_Quickcheck "Char")
    1.18 +
    1.19 +setup {*
    1.20 +  fold String_Code.add_literal_char ["Haskell_Quickcheck"] 
    1.21 +  #> String_Code.add_literal_list_string "Haskell_Quickcheck"
    1.22 +*}
    1.23 +
    1.24 +code_instance char :: equal
    1.25 +  (Haskell_Quickcheck -)
    1.26 +
    1.27 +code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    1.28 +  (Haskell_Quickcheck infix 4 "==")
    1.29 +
    1.30  subsubsection {* Type @{text "code_int"} for Haskell_Quickcheck's Int type *}
    1.31  
    1.32  typedef (open) code_int = "UNIV \<Colon> int set"