define bff on a partial getlen
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 28 Jan 2014 14:15:12 +0000 (15:15 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 28 Jan 2014 14:15:12 +0000 (15:15 +0100)
commit1c3da162d500cfe885fa21b4d75847c4bcbb2aa1
tree75af4c2ff1fc049ea0a0b02b2104c16a93ab3d6a
parentb0eb7ada208d33eb82ec27cb7d40b9fa59646c92
define bff on a partial getlen

The representation chosen is to give both an injection gl₁ and a
function gl₂ (formerly getlen), such that by choosing a non-identity for
gl₁ partiality of getlen can be expressed. An alternative would have
been to allow getlen to return a Maybe ℕ and have get return
  maybe (Vec A) ⊤ (getlen n)
thus sending all inputs for which getlen yields nothing to tt. It seems
that while there is no way to obtain a such a getlen predicate from an
arbitrary index Setoid I, it should be possible to manufacture a Setoid
from a predicate. Thanks to Stefan Mehner for the insightful discussion.
BFF.agda
FreeTheorems.agda