summaryrefslogtreecommitdiff
path: root/Everything.agda
diff options
context:
space:
mode:
authorHelmut Grohne <grohne@cs.uni-bonn.de>2014-02-10 16:27:41 +0100
committerHelmut Grohne <grohne@cs.uni-bonn.de>2014-02-10 16:27:41 +0100
commite545ac3a23792e1905bf1b4aedb1f96ebb5a9e90 (patch)
treecb5d9e1be44789574c8d3516fddf0e974a6007fe /Everything.agda
parent6cc566c46889c5e7aafc8d75c6627137e56ab30f (diff)
downloadbidiragda-e545ac3a23792e1905bf1b4aedb1f96ebb5a9e90.tar.gz
add bffplug and bffinv functions and examples
We can now exploit getlen being rightinvertible and it works for drop and sieve.
Diffstat (limited to 'Everything.agda')
-rw-r--r--Everything.agda1
1 files changed, 1 insertions, 0 deletions
diff --git a/Everything.agda b/Everything.agda
index e1734a9..e37c76e 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -11,3 +11,4 @@ import Bidir
import LiftGet
import Precond
import Examples
+import BFFPlug