formulate theorem-1
authorHelmut Grohne <helmut@subdivi.de>
Sun, 22 Jan 2012 21:43:32 +0000 (22:43 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Sun, 22 Jan 2012 21:43:32 +0000 (22:43 +0100)
Bidir.agda

index e77de94..ff20caf 100644 (file)
@@ -92,3 +92,6 @@ bff get eq s v = let s′ = idrange (length s)
                      h  = assoc eq (get s′) v
                      h′ = maybe′ (λ jh → just (union jh g)) nothing h
                  in maybe′ (λ jh′ → just (map (flip lookup jh′) s′)) nothing h′
+
+theorem-1 : (get : {α : Set} → List α → List α) → {τ : Set} → (eq : (x y : τ) → Dec (x ≡ y)) → (s : List τ) → bff get eq s (get s) ≡ just s
+theorem-1 get eq s = {!!}