issues
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
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Code generation failure in tests
#52
runKleisli
opened
6 years ago
0
Packaging
#51
runKleisli
closed
6 years ago
0
Spansl/z no longer considered in the project. Hopefully with type sys…
#50
runKleisli
closed
6 years ago
0
No significant eliminated matrix finishes computing
#49
runKleisli
opened
6 years ago
1
%default total
#48
runKleisli
closed
6 years ago
1
Generalized algebraic assumptions
#47
runKleisli
opened
6 years ago
1
Better tactics
#46
runKleisli
opened
6 years ago
0
Newer version of Idris
#45
runKleisli
opened
6 years ago
0
Splitting work into more general modules
#44
runKleisli
opened
6 years ago
0
Basic refactoring
#43
runKleisli
opened
6 years ago
0
Move existing modules
#42
runKleisli
closed
6 years ago
0
Modulo
#41
runKleisli
closed
6 years ago
1
Connect bezout's identity to gaussian elimination
#40
runKleisli
closed
6 years ago
0
Archive original GCD exploratory work
#39
runKleisli
closed
6 years ago
0
Bezout's identity for ZZ
#38
runKleisli
closed
6 years ago
0
Nohumans - totality
#37
runKleisli
closed
6 years ago
0
Nohumans
#36
runKleisli
closed
6 years ago
0
Instance resolution problem work
#35
runKleisli
closed
6 years ago
0
FinOrdering work
#34
runKleisli
closed
6 years ago
0
Row echelon work - Crown redo the new ZZGaussianElimination
#33
runKleisli
closed
6 years ago
0
Row echelon work - complete arc
#32
runKleisli
closed
6 years ago
0
Gaussian elimination redo
#31
runKleisli
closed
6 years ago
0
Docsupd zzgauss lemmas
#30
runKleisli
closed
7 years ago
0
ZZGauss fixup
#29
runKleisli
closed
7 years ago
0
ZZModuleSpan work - Update docs & complete
#28
runKleisli
closed
7 years ago
0
ZZModuleSpan complete
#27
runKleisli
closed
7 years ago
0
ZZModuleSpan work stable point - alg-nullcol-perms
#26
runKleisli
closed
7 years ago
0
ZZModuleSpan work stable point
#25
runKleisli
closed
8 years ago
0
Identify identical expressions where typeclass resolution fails to identify instances
#24
runKleisli
closed
6 years ago
2
Dangling structural and algebraic
#23
runKleisli
closed
8 years ago
0
Close all relevant holes in Data.Matrix.LinearCombinations
#22
runKleisli
closed
8 years ago
0
Figure out how to deduce a (rowEchelon xs)'s type at an index where the row of (xs) is known
#21
runKleisli
closed
6 years ago
2
ZZGauss lemmas - retry
#20
runKleisli
closed
8 years ago
0
Revert "ZZGauss lemmas"
#19
runKleisli
closed
8 years ago
0
ZZGauss lemmas
#18
runKleisli
closed
8 years ago
0
Matrix algebraic proofs
#17
runKleisli
closed
8 years ago
0
Delete zero rows
#16
runKleisli
opened
8 years ago
0
Gaussian elimination induction
#15
runKleisli
closed
8 years ago
0
Gauss related arguments
#14
runKleisli
closed
8 years ago
0
Further spans properties
#13
runKleisli
closed
8 years ago
0
Define ZZ gaussian elimination
#12
runKleisli
closed
8 years ago
0
spanslztrans work
#11
runKleisli
closed
8 years ago
0
New linear combinations module
#10
runKleisli
closed
8 years ago
0
Thm: timesMatMatAsMultipleLinearCombos
#9
runKleisli
closed
8 years ago
0
recombine-10June-2
#8
runKleisli
closed
8 years ago
0
recombine-10June
#7
runKleisli
closed
8 years ago
0
Feature request: better-than-cong for applying Leibniz to m equalities with (m+k)-ary function
#6
runKleisli
opened
8 years ago
1
Circularity between flipIsInvolutionExtensional and etaBinary
#5
runKleisli
closed
6 years ago
1
Write compressMonoidsum and friends better
#4
runKleisli
opened
8 years ago
0
recombine-09June-2
#3
runKleisli
closed
8 years ago
0
Next