# HG changeset patch # User haftmann # Date 1482520347 -3600 # Node ID f77b946d18aa6c72bef0724b1a3b722fc47d31e5 # Parent ce441970956fe94ce67064763541d83bed688412 restored instance for char, which got ancidentally lost in b3f2b8c906a6 diff -r ce441970956f -r f77b946d18aa src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Fri Dec 23 20:10:38 2016 +0100 +++ b/src/HOL/Quickcheck_Exhaustive.thy Fri Dec 23 20:12:27 2016 +0100 @@ -476,13 +476,18 @@ end -(* FIXME instantiation char :: check_all +instantiation char :: check_all begin -definition - "check_all f = check_all (\(x, t1). check_all (\(y, t2). - f (Char x y, \_. Code_Evaluation.App - (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))" +primrec check_all_char' :: + "(char \ (unit \ term) \ (bool \ term list) option) \ char list \ (bool \ term list) option" + where "check_all_char' f [] = None" + | "check_all_char' f (c # cs) = f (c, \_. Code_Evaluation.term_of c) + orelse check_all_char' f cs" + +definition check_all_char :: + "(char \ (unit \ term) \ (bool \ term list) option) \ (bool \ term list) option" + where "check_all f = check_all_char' f Enum.enum" definition enum_term_of_char :: "char itself \ unit \ term list" where @@ -490,7 +495,7 @@ instance .. -end *) +end instantiation option :: (check_all) check_all begin