equal
deleted
inserted
replaced
16 |
16 |
17 definition |
17 definition |
18 "set_bits f = |
18 "set_bits f = |
19 (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then |
19 (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then |
20 let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' |
20 let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' |
21 in bl_to_bin (rev (map f [0..<n])) |
21 in horner_sum of_bool 2 (map f [0..<n]) |
22 else if \<exists>n. \<forall>n'\<ge>n. f n' then |
22 else if \<exists>n. \<forall>n'\<ge>n. f n' then |
23 let n = LEAST n. \<forall>n'\<ge>n. f n' |
23 let n = LEAST n. \<forall>n'\<ge>n. f n' |
24 in sbintrunc n (bl_to_bin (True # rev (map f [0..<n]))) |
24 in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) |
25 else 0 :: int)" |
25 else 0 :: int)" |
26 |
26 |
27 instance .. |
27 instance .. |
28 |
28 |
29 end |
29 end |