• Ralf Jung's avatar
    Remove the `default` notation for options · e585be6d
    Ralf Jung authored
    The notation was parsing-only and all it did was reorder the arguments for
    from_option.  This creates just a needless divergence between what is written
    and what is printed.  Also, removing it frees the name for maybe introducing a
    function or notation `default` with a type like `T -> option T -> T`.
    e585be6d
Name
Last commit
Last update
..
base.v Loading commit data...
bset.v Loading commit data...
coPset.v Loading commit data...
collections.v Loading commit data...
countable.v Loading commit data...
decidable.v Loading commit data...
fin.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...
functions.v Loading commit data...
gmap.v Loading commit data...
gmultiset.v Loading commit data...
hashset.v Loading commit data...
hlist.v Loading commit data...
infinite.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...
namespaces.v Loading commit data...
nat_cancel.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...
set.v Loading commit data...
sorting.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...