allow shape shape updates in bff
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 7 Feb 2014 15:15:03 +0000 (16:15 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 7 Feb 2014 15:15:03 +0000 (16:15 +0100)
commit586d72e18898311d975f5748bca397c403b6a83b
tree2733f576b6e3ff0965ca8eb213fe0635be3631df
parent95609983219f14e8f4c0758cd0688b984d8b1455
allow shape shape updates in bff

Unlike the original version in VoigtlaenderHMW13, we do not request an
  sput : ℕ → ℕ → Maybe ℕ
function for determining the updated source shape from the original
source and updated view shape. Instead we ask the caller directly to
provide the result of sput together with a proof that its getlen matches
with the provided, updated view.

The precondition assoc-enough is not enriched in this way and still
requires a non-changing shape. I.e. it says what it said before.
BFF.agda
Bidir.agda
FinMap.agda
Precond.agda