Refactor operations - Githubissues

JamesGallicchio / LeanColls

WIP collections library for Lean 4

Apache License 2.0

30 stars 7 forks source link

Open JamesGallicchio opened 7 months ago

JamesGallicchio commented 7 months ago

Big refactor of Ops.lean.

Improves class names to be consistent/predictable
Refactors Fold correctness to be in terms of ToMultiset instead of list permutations. This includes some lemmas about multiset induction to prove properties of a fold.
Adds ToSet class as the top of the collection model hierarchy

JamesGallicchio commented 7 months ago

Need to add deprecation notices to all the names that have been changed (eek)