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

Packaging #51

Closed runKleisli closed 6 years ago

runKleisli commented 6 years ago

FinOrdering --> Data.Fin.FinOrdering

FinStructural --> Data.Fin.Structural

ZZModuleSpan --> Data.Matrix.ZZModuleSpan

ZZDivisors --> Control.Algebra.ZZDivisors

Control.Algebra.ModuloVerification --> Data.ZZ.ModuloVerification

ZZModulo --> Data.ZZ.ZZModulo

ZZBezoutsIdentity --> Control.Algebra.ZZBezoutsIdentity

ZZGCDOfVectAlg --> Control.Algebra.ZZGCDOfVectAlg

RowEchelon --> Data.Matrix.RowEchelon

ZZGaussianEliminationLemmas --> Data.Matrix.ZZGaussianEliminationLemmas

ZZGaussianElimination --> Data.Matrix.ZZGaussianElimination

ZZGaussianEliminationNoMonad --> Data.Matrix.ZZGaussianEliminationNoMonad