• Robbert Krebbers's avatar
    Revert "prelude: add notation for > and >= for all kinds of numbers" · eb563833
    Robbert Krebbers authored
    This reverts commit 24fa20e5.
    
    Although these symmetric variants sometimes look "better", they
    are really annoying and should IMHO never be used:
    
    1.) For lemmas there is now a choice between >= and <=. Since there is
    no longer a canonical choice, it is very easy to introduce a lot of
    inconsistencies in statements of lemmas.
    
    2.) For automation the situation becomes annoying, you have to built in
    stuff for both >= and <=. That is very error-prone.
    
    3.) For N and Z the notions x <= y and y >= x are not even convertible!
    That means that done/by does not solve x <= y if you have y >= x and if
    avoids you applying certain lemmas.
    eb563833
Name
Last commit
Last update
..
base.v Loading commit data...
bsets.v Loading commit data...
co_pset.v Loading commit data...
collections.v Loading commit data...
countable.v Loading commit data...
decidable.v Loading commit data...
error.v Loading commit data...
fin_collections.v Loading commit data...
fin_map_dom.v Loading commit data...
fin_maps.v Loading commit data...
finite.v Loading commit data...
gmap.v Loading commit data...
hashset.v Loading commit data...
lexico.v Loading commit data...
list.v Loading commit data...
listset.v Loading commit data...
listset_nodup.v Loading commit data...
mapset.v Loading commit data...
natmap.v Loading commit data...
nmap.v Loading commit data...
numbers.v Loading commit data...
option.v Loading commit data...
orders.v Loading commit data...
pmap.v Loading commit data...
prelude.v Loading commit data...
pretty.v Loading commit data...
proof_irrel.v Loading commit data...
relations.v Loading commit data...
sets.v Loading commit data...
streams.v Loading commit data...
stringmap.v Loading commit data...
strings.v Loading commit data...
tactics.v Loading commit data...
vector.v Loading commit data...
zmap.v Loading commit data...