agda-stdlib
agda-stdlib copied to clipboard
agda
The Agda standard library
I defined my ≤-Induction without needing to create a new inequality for that.
This PR introduces `Algebra.Linear.VectorSpace`, an abstract vector space. The purpose of this new type is to provide the familiar metaphor/interface of "vector/matrix" that people are used to using in their...
Hello there. I would like to explore a contribution to the standard library. I have a few DivMod proofs that I use all the time and that I think others...
In this PR - Correct definitions `LeftBol` and `IsMoufangLoop` Show the following for MoufangLoop - `leftAlternative : LeftAlternative _∙_` - `rightAlternative : RightAlternative _∙_` - `alternative : Alternative _∙_` -...
This is largely preliminaries for #1741, which I'm still playing with how to implement.
Work on issue #1116 . So far, this only concerns the problem that deBruijn-indices have to be adjusted when using the forall-version of the solver macro.
Currently the reflective interface for `Tactic.RingSolver` only works over concrete instances of rings (see https://github.com/oisdk/agda-ring-solver/issues/12). It would be useful to get this working for generic rings as well.
I just realize the library does not have comparison returning ``. is it actually the case or I just over looked?
I propose the following two backwards compatible additions. (1) To add to ``Function.Injection`` ``` InjectiveBy≡ : ∀ {a b} {A : Set a} {B : Set b} → (A →...
