def: Fin as a record type

[plt-amy]

Reimplement Fin n as a pair of a natural k + an irrelevant proof that k < n, using a view to preserve the structure of pattern-matching proofs. A couple proofs need to appeal to the view for the coverage checker to see that only fzero is possible.

[Lavenza]

Pull request preview

Changed pages

• Data.Fin.Base (+195, -156)
• Data.Fin.Properties (+147, -160)
• Data.Fin.Closure (+112, -99)
• Data.Maybe.Properties (+67, -24)
• Data.Fin.Product (+22, -16)
• Data.Nat.Prime (+9, -20)
• Algebra.Group.Instances.Cyclic (+10, -13)
• Data.Fin.Finite (+17, -6)
• Data.Nat.Base (+22, -0)
• Data.List.Membership (+11, -8)
• Logic.Propositional.Classical.SAT (± 9)
• Cat.Diagram.Product.Finite (+9, -6)
• Data.Nat.Order (+0, -15)
• Data.Nat.Solver (+8, -6)
• Logic.Propositional.Classical (+7, -5)
• Cat.Instances.Shape.Cospan (+5, -6)
• Algebra.Ring.Module.Multilinear (+4, -6)
• Data.Maybe.Base (+10, -0)
• Data.Rational.Base (+6, -4)
• Data.Vec.Properties (+6, -4)

[ncfavier]

Very nice!