restored instance for char, which got ancidentally lost in b3f2b8c906a6
authorhaftmann
Fri Dec 23 20:12:27 2016 +0100 (2016-12-23)
changeset 64670f77b946d18aa
parent 64669 ce441970956f
child 64671 93e375bd3283
restored instance for char, which got ancidentally lost in b3f2b8c906a6
src/HOL/Quickcheck_Exhaustive.thy
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Dec 23 20:10:38 2016 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Dec 23 20:12:27 2016 +0100
     1.3 @@ -476,13 +476,18 @@
     1.4  
     1.5  end
     1.6  
     1.7 -(* FIXME instantiation char :: check_all
     1.8 +instantiation char :: check_all
     1.9  begin
    1.10  
    1.11 -definition
    1.12 -  "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
    1.13 -     f (Char x y, \<lambda>_. Code_Evaluation.App
    1.14 -       (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
    1.15 +primrec check_all_char' ::
    1.16 +  "(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> char list \<Rightarrow> (bool \<times> term list) option"
    1.17 +  where "check_all_char' f [] = None"
    1.18 +  | "check_all_char' f (c # cs) = f (c, \<lambda>_. Code_Evaluation.term_of c)
    1.19 +      orelse check_all_char' f cs"
    1.20 +
    1.21 +definition check_all_char ::
    1.22 +  "(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool \<times> term list) option"
    1.23 +  where "check_all f = check_all_char' f Enum.enum"
    1.24  
    1.25  definition enum_term_of_char :: "char itself \<Rightarrow> unit \<Rightarrow> term list"
    1.26  where
    1.27 @@ -490,7 +495,7 @@
    1.28  
    1.29  instance ..
    1.30  
    1.31 -end *)
    1.32 +end
    1.33  
    1.34  instantiation option :: (check_all) check_all
    1.35  begin