equal
deleted
inserted
replaced
56 |
56 |
57 constdefs |
57 constdefs |
58 fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a" |
58 fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a" |
59 "fold f e A == @x. (A,x) : foldSet f e" |
59 "fold f e A == @x. (A,x) : foldSet f e" |
60 |
60 |
61 setsum :: "('a => 'b) => 'a set => ('b::plus_ac0)" |
61 setsum :: "('a => 'b) => 'a set => ('b::{plus, zero})" |
62 "setsum f A == if finite A then fold (op+ o f) 0 A else 0" |
62 "setsum f A == if finite A then fold (op+ o f) 0 A else 0" |
63 |
63 |
64 locale LC = |
64 locale LC = |
65 fixes |
65 fixes |
66 f :: ['b,'a] => 'a |
66 f :: ['b,'a] => 'a |