equal
deleted
inserted
replaced
103 |
103 |
104 lemma |
104 lemma |
105 [code]: "cps_of_set (set xs) f = find_first f xs" |
105 [code]: "cps_of_set (set xs) f = find_first f xs" |
106 sorry |
106 sorry |
107 |
107 |
108 consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option" |
108 consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option" |
109 consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => code_numeral => term list Quickcheck_Exhaustive.three_valued" |
109 consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued" |
110 |
110 |
111 lemma |
111 lemma |
112 [code]: "pos_cps_of_set (set xs) f i = find_first f xs" |
112 [code]: "pos_cps_of_set (set xs) f i = find_first f xs" |
113 sorry |
113 sorry |
114 |
114 |