-
Notifications
You must be signed in to change notification settings - Fork 11
Open
Labels
enhancementNew feature or requestNew feature or requestgood first issueGood for newcomersGood for newcomershelp wantedExtra attention is neededExtra attention is needed
Description
Context
CompPoly/Fields/Binary/Tower/Basic.lean includes a TODO near towerAlgebraMap:
migrate to Fin.dfoldl
Proposed work
- Refactor
towerAlgebraMapto useFin.dfoldlinstead of the current recursive style. - Keep theorem statements/API unchanged.
Acceptance criteria
- Existing callers of
towerAlgebraMaprequire no API changes. - proofs and/or tests to show correctness
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
enhancementNew feature or requestNew feature or requestgood first issueGood for newcomersGood for newcomershelp wantedExtra attention is neededExtra attention is needed