From 347f4ff2ed76a0fc5648faf698b054efba51e0ff Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Sun, 22 Jan 2012 22:43:32 +0100
Subject: formulate theorem-1

---
 Bidir.agda | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'Bidir.agda')

diff --git a/Bidir.agda b/Bidir.agda
index e77de94..ff20caf 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -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 = {!!}
-- 
cgit v1.2.3