]> matita.cs.unibo.it Git - helm.git/commit
There used to be two minimal joins between an ordered_set and an abelian_group:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 2 Jan 2007 20:05:21 +0000 (20:05 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 2 Jan 2007 20:05:21 +0000 (20:05 +0000)
commit06a089726af079d5b2fe42ba78632565dad0eb3e
tree4b25fae3acb261eb4247e8402ba7c22be596795b
parent780dd584632c362a0cd01149e23766b62037c971
There used to be two minimal joins between an ordered_set and an abelian_group:
ordered_field_ch0 and riesz_space. To avoid the problem without introducing
backtracking in unification I have introduced ordered_abelian_groups.
An ordered_field_ch0 is recast as a field that is also an ordered_abelian_group
and a cotransitively_ordered_set. I still have to recast riesz_spaces as
vector spaces that are also ordered_abelian_groups and lattices.
matita/dama/ordered_fields_ch0.ma
matita/dama/ordered_groups.ma [new file with mode: 0644]