summaryrefslogtreecommitdiff
path: root/GetTypes.agda
diff options
context:
space:
mode:
authorHelmut Grohne <grohne@cs.uni-bonn.de>2014-01-30 14:23:10 +0100
committerHelmut Grohne <grohne@cs.uni-bonn.de>2014-01-30 14:23:10 +0100
commite227314c11a17efa2e41ee8756041c4e5b747792 (patch)
tree1c0c8b7a6643aabb4fe5d9cd46a333b5db7158f1 /GetTypes.agda
parentffd72d6471ec0166b4dcb4f6b622bcc1c4aafcbf (diff)
downloadbidiragda-e227314c11a17efa2e41ee8756041c4e5b747792.tar.gz
fully allow partial get functions
By choosing gl₁ = suc and gl₂ = id, the tail function can now be bidirectionalized.
Diffstat (limited to 'GetTypes.agda')
0 files changed, 0 insertions, 0 deletions