summaryrefslogtreecommitdiff
path: root/BFFPlug.agda
AgeCommit message (Collapse)Author
2018-11-25port to agda/2.5.4.1 and agda-stdlib/0.17Helmut Grohne
2018-11-25reorganize equality importsHelmut Grohne
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.
2015-06-09drop barred members from GetTypesHelmut Grohne
These became duplicates of their non-barred counterparts.
2015-06-09drop the Function.Equality requirement from GetTypesHelmut Grohne
We never used the equality property. Thus a simple function is sufficient here. We always fulfilled the property using ≡-to-Π anyway.
2014-09-26resolve ambiguity in BFFPlugHelmut Grohne
Fixes compilation with Agda 2.4.2.
2014-02-26remove the sequenceV call from bffHelmut Grohne
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.
2014-02-17use drop, tail and take from Data.Vec in examplesHelmut Grohne
This is possible using the PartialVecVec implementation.
2014-02-17switch examples to PartialVecVecHelmut Grohne
2014-02-14add back original bff function before shape updatesHelmut Grohne
2014-02-10add bffplug and bffinv functions and examplesHelmut Grohne
We can now exploit getlen being rightinvertible and it works for drop and sieve.