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

Spansl/z no longer considered in the project. Hopefully with type sys… #50

Closed runKleisli closed 6 years ago

runKleisli commented 6 years ago

…tems more flexible for algebraic hierarchy we can come back to this. Perhaps Setoids allow the theorems to work for all modules, but that would be a change of system of linear algebra.