summaryrefslogtreecommitdiff
path: root/BFFPlug.agda
AgeCommit message (Collapse)Author
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.