add bffplug and bffinv functions and examples
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 10 Feb 2014 15:27:41 +0000 (16:27 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 10 Feb 2014 15:27:41 +0000 (16:27 +0100)
commite545ac3a23792e1905bf1b4aedb1f96ebb5a9e90
treecb5d9e1be44789574c8d3516fddf0e974a6007fe
parent6cc566c46889c5e7aafc8d75c6627137e56ab30f
add bffplug and bffinv functions and examples

We can now exploit getlen being rightinvertible and it works for drop
and sieve.
BFFPlug.agda [new file with mode: 0644]
Everything.agda