fully allow partial get functions
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 30 Jan 2014 13:23:10 +0000 (14:23 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 30 Jan 2014 13:23:10 +0000 (14:23 +0100)
commite227314c11a17efa2e41ee8756041c4e5b747792
tree1c0c8b7a6643aabb4fe5d9cd46a333b5db7158f1
parentffd72d6471ec0166b4dcb4f6b622bcc1c4aafcbf
fully allow partial get functions

By choosing gl₁ = suc and gl₂ = id, the tail function can now be
bidirectionalized.
Bidir.agda
Precond.agda