A library for doing linear algebra in Agda. With this library, it is possible to normalize a matrix using Gauss Elimination. See this file example. There are also some proofs that the normalization algorithm works. Look also at the API example to see how the main data types are used in this project.
Clone the repository and inside the project directory run these commands:
Get the nix environment:
nix develop
Compile agda files:
agda src/EverythingUseful.agda
- See Typst website to understand how Typst works.
- It is not possible to compile Typst documents using Nix, but if you have Typst installed in your machine, you can run to visualize the documentation:
typst compile main.typ