Dangling structural and algebraic - Githubissues

runKleisli / verified-integer-gaussian-elimination

Idris package defining, implementing, and verifying naiive Gaussian elimination over the integers in some system of linear algebra.

Other

9 stars 0 forks source link

Dangling structural and algebraic #23

Closed runKleisli closed 8 years ago

runKleisli commented 8 years ago

Prove many basic identities about (Vect)s, matrices, and the algebra of ZZ and (Vect)s/matrices thereof.

Results:

No holes in Control.Algebra.ZZVerifiedInstances.
Only holes in Data.Vect.Structural are equalities true by definition but where instance resolution failed for the classes some terms are methods of.
Only holes in Data.Matrix.Structural come from Data.Matrix.AlgebraicVerified or Data.Vect.Structural and are of the same kind as in Data.Vect.Structural.