|
969
|
1 |
Rec = Fixedpt +
|
|
|
2 |
consts
|
|
1476
|
3 |
fix :: ('a=>'a) => 'a
|
|
|
4 |
Dom :: (('a=>'b) => ('a=>'b)) => 'a set
|
|
|
5 |
Domf :: (('a=>'b) => ('a=>'b)) => 'a set => 'a set
|
|
969
|
6 |
rules
|
|
|
7 |
Domf_def "Domf(F,D) == {y . !f g. (!x:D. f(x)=g(x)) --> F(f,y)=F(g,y)}"
|
|
|
8 |
Dom_def "Dom(F) == lfp(Domf(F))"
|
|
|
9 |
end
|