search

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

Gauss related arguments #14

Closed runKleisli closed 8 years ago

runKleisli commented 8 years ago

Implement (elimFirstCol), the base case of gaussian elimination, by which the leftmost column is eliminated, introducing constructions like (foldAutoind2) and organizing many of the lemmas into modules along the way.