From e2072c8146ecb1e33ea2823bc26e76ea607f10c5 Mon Sep 17 00:00:00 2001 From: Leif Warner Date: Thu, 29 Sep 2016 20:56:32 -0700 Subject: [PATCH] Ensure references in VerifiedComonad are properly qualified. Added back the proof for Store. --- Lens.idr | 27 +++++++++------------------ 1 file changed, 9 insertions(+), 18 deletions(-) diff --git a/Lens.idr b/Lens.idr index af7b487..2270141 100644 --- a/Lens.idr +++ b/Lens.idr @@ -3,6 +3,7 @@ module Lens import Control.Category %access public export +%default total -- Store comonad @@ -14,14 +15,14 @@ interface Functor w => Comonad (w : Type -> Type) where interface Comonad w => VerifiedComonad (w : Type -> Type) where comonadLaw1 : (wa : w a) -> - extend extract wa = wa + Lens.extend Lens.extract wa = wa comonadLaw2 : (f : w a -> b) -> (wa : w a) -> - extract (extend f wa) = f wa + Lens.extract (Lens.extend f wa) = f wa comonadLaw3 : (f : w b -> c) -> (g : w a -> b) -> (wa : w a) -> - extend f (extend g wa) = extend (\d => f (extend g d)) wa + Lens.extend f (Lens.extend g wa) = Lens.extend (\d => f (Lens.extend g d)) wa Functor (Store s) where map f (MkStore g a) = MkStore (f . g) a @@ -30,21 +31,11 @@ Comonad (Store s) where extract (MkStore f a) = f a extend f (MkStore g a) = MkStore (\b => f (MkStore g b)) a --- VerifiedComonad (Store s) where --- comonadLaw1 (MkStore f a) = ?storeIdentityProof --- comonadLaw2 f (MkStore g a) = Refl --- comonadLaw3 f g (MkStore h a) = Refl - --- -- TODO: This is evil. --- -- Supposedly (jonsterling) this definition used to work without the believe_me. --- private --- eta : (f : a -> b) -> f = (\c => f c) --- eta g = believe_me Refl {g} - --- storeIdentityProof = proof --- intros --- rewrite eta f --- trivial + +VerifiedComonad (Store s) where + comonadLaw1 (MkStore f a) = Refl + comonadLaw2 f (MkStore g a) = Refl + comonadLaw3 f g (MkStore h a) = Refl pos : Store s a -> s pos (MkStore _ s) = s