• Robbert Krebbers's avatar
    Hack to avoid getting String.length instead of List.length. · 26d86662
    Robbert Krebbers authored
    In noticed in Amin's development that importing the proof mode often
    turns length into String.length. The weird thing is that before importing
    the proof mode, it refers to List.length, and when importing just the
    proof mode, it refers to List.length too. However, in some combinations of
    imports, it seems to result in it refering to String.length...
    26d86662
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...
functions.v Loading commit data...
gmap.v Loading commit data...
hashset.v Loading commit data...
hlist.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...