Make lemmas for `seq` and `seqZ` consistent.

This closes issue #57 (closed)

added 1 commit

• 6933feef - CHANGELOG.

Compare with previous version

changed the description

added 1 commit

• 6b11b096 - CHANGELOG.

Compare with previous version

resolved all threads

mentioned in commit f0bede87

merged

Cc @iris-users -- if you are using one of the methods mentioned in the changelog here, you'll have to adjust your code.

In case it's useful to anybody, here's a sed script with all the renames for stdpp 1.3.0 (should work on macOS and Linux):

stdpp-master.sed:

s/\bfmap_seq\b/fmap_S_seq/g
s/\blookup_seq\b/lookup_seq_lt/g
s/\blookup_seq\b/lookup_seq_lt/g
s/\blookup_seq_inv\b/lookup_seq/g
s/\bseqZ_lookup_lt\b/lookup_seqZ_lt/g
s/\bseqZ_lookup_ge\b/lookup_seqZ_ge/g
s/\bseqZ_lookup\b/lookup_seqZ/g
s/\bvec_to_list_of_list\b/vec_to_list_to_vec/g
s/\bfin_of_nat\b/nat_to_fin/g
s/\bfin_to_of_nat\b/fin_to_nat_to_fin/g
s/\bfin_of_to_nat\b/nat_to_fin_to_nat/g

run with:

find . -name '*.v' -exec sed -f stdpp-master.sed -i~ {} \;

Thanks @tchajed! However, I think the lookup_seq_inv -> lookup_seq rename is missing.

Ah yes, I wanted it to be idempotent, but maybe we should give that up.