ryanorendorff/functional-linear-algebra

Formalizing linear algebra in Agda by representing matrices as functions

functional-linear-algebra's Issues

Fails to build with Agda 2.6.4

/build/source/src/FLA/Algebra/LinearMap/Properties.agda:101,7-11
f[u+v]≡f[u]+f[v]ᶜ u v != f[u+v]≡f[u]+f[v]ᵈ u v of type
f (u +ⱽ v) ≡ f u +ⱽ f v
when checking that the expression refl has type
record
{ f = f
; f[u+v]≡f[u]+f[v] = f[u+v]≡f[u]+f[v]ᶜ
; f[c*v]≡c*f[v] = f[c*v]≡c*f[v]ᶜ
}
≡
record
{ f = f
; f[u+v]≡f[u]+f[v] = f[u+v]≡f[u]+f[v]ᵈ
; f[c*v]≡c*f[v] = f[c*v]≡c*f[v]ᵈ
}

Support agda-stdlib 2

This library fails to build with agda-stdlib 2.0:

/build/source/src/FLA/Algebra/LinearAlgebra/Properties.agda:44,45-47
A !=< ℕ
when checking that the expression 0ᶠ has type ℕ

Does not build anymore with standard library 1.5

Standard library was released at version 1.5 agda/agda-stdlib#1386 🎉

This package doesn't build anymore with the up to date standard library:

     Checking FLA.Algebra.LinearAlgebra.Properties (/build/source/src/FLA/Algebra/LinearAlgebra/Properties.agda).
      Checking FLA.Data.Vec.Properties (/build/source/src/FLA/Data/Vec/Properties.agda).
  /build/source/src/FLA/Algebra/LinearAlgebra/Properties.agda:53,32-49
  Ambiguous name zipWith-replicate. It could refer to any one of
    Data.Vec.Properties.zipWith-replicate bound at
      /nix/store/dc087m2w1bmjjhv13m3r6zg8drmxivg7-standard-library-1.5/src/Data/Vec/Properties.agda:698,1-18
    FLA.Data.Vec.Properties.zipWith-replicate bound at
      /build/source/src/FLA/Data/Vec/Properties.agda:128,1-18
  (hint: Use C-c C-w (in Emacs) if you want to know why)
  when scope checking zipWith-replicate

Found via NixOS/nixpkgs#110830

Release to nixpkgs?

It would be great if this package is also on nixpkgs. Do you want to put it there? I can advise on how to do that, and review.

Release a version compatible with standard-library 1.7 and Agda 2.6.2

Currently the version is pinned to 1.6, which gives this error message if you try to build with 1.7:

 Library 'standard-library-1.6' not found.