| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Since we are working with multiple setoids now, it makes more sense to
qualify their members. Follow the "as P" pattern from the standard
library. Also stop importing those symbols from Relation.Binary.Core as
later agda-stdlib versions will move them away. Rather than EqSetoid or
PropEq, use P.setoid consistently.
|
|
These became duplicates of their non-barred counterparts.
|
|
We never used the equality property. Thus a simple function is
sufficient here. We always fulfilled the property using ≡-to-Π anyway.
|
|
Fixes compilation with Agda 2.4.2.
|
|
This allows bff to be more precise with regard to its failure modes,
even though we are not yet making use of that projected precision. It
allows inserting a default value for entries that could not be recovered
in a shape changing update as described in VoigtlaenderHMW13.
|
|
This is possible using the PartialVecVec implementation.
|
|
|
|
|
|
We can now exploit getlen being rightinvertible and it works for drop
and sieve.
|
