From e38d00d4a31cf3fe88646ff128cf0b8511354c21 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Thu, 19 Oct 2023 13:52:45 -0400 Subject: [PATCH] Fix typos --- src/Control/Lens/Cons.idr | 4 ++-- src/Data/Maybe/Lens.idr | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Control/Lens/Cons.idr b/src/Control/Lens/Cons.idr index 01e0f02..65c279b 100644 --- a/src/Control/Lens/Cons.idr +++ b/src/Control/Lens/Cons.idr @@ -14,7 +14,7 @@ import Control.Lens.Optional ||| left side of a sequence. public export interface Cons s t a b | s where - ||| An isomorphism that can inspact the left side of a sequence. + ||| An isomorphism that can inspect the left side of a sequence. consIso : Iso s t (Maybe (a, s)) (Maybe (b, t)) ||| A prism that can attach or detach a value from the left side of a @@ -45,7 +45,7 @@ nil = review consIso Nothing ||| right side of a sequence. public export interface Snoc s t a b | s where - ||| An isomorphism that can inspact the right side of a sequence. + ||| An isomorphism that can inspect the right side of a sequence. snocIso : Iso s t (Maybe (s, a)) (Maybe (t, b)) ||| This is a prism that can attach or detach a value from the right side of a diff --git a/src/Data/Maybe/Lens.idr b/src/Data/Maybe/Lens.idr index fa0b9ca..9f0eaad 100644 --- a/src/Data/Maybe/Lens.idr +++ b/src/Data/Maybe/Lens.idr @@ -22,7 +22,7 @@ Just_ = prism Just $ \case infixl 9 .? ||| The composition `l .? l'` is equivalent to `l . Just_ . l'`. -||| Useful for optics who focus type is a `Maybe`, such as `at`. +||| Useful for optics whose focus type is a `Maybe`, such as `at`. public export (.?) : IsPrism p => Optic' p s t (Maybe a) (Maybe b) -> Optic' p a b a' b' -> Optic' p s t a' b' l .? l' = l . Just_ . l'