Skip to content

All list "map singleton" lemmas consistently use `singletonM` in their name

Ralf Jung requested to merge ralf/list-singleton into master

I implemented @robbertkrebbers' proposal for naming. This is a breaking change; the following sed script helps port things that work with current master:

s/\blist_singleton_core\b/list_singletonM_core/g
s/\blist_lookup_singleton(|_lt|_gt|_ne)\b/list_lookup_singletonM\1/g
s/\blist_singleton_(validN|length)\b/list_singletonM_\1/g
s/\blist_alter_singleton\b/list_alter_singletonM/g
s/\blist_singleton_included\b/list_singletonM_included/g
s/\blist_singleton_updateP\b/list_singletonM_updateP/
s/\blist_singleton_snoc\b/list_singletonM_snoc/

Fixes #309 (closed)

Edited by Ralf Jung

Merge request reports