toki/idris2-lens
1
0
Fork 0
Code Issues Pull requests Activity

Fix typos

Browse source
This commit is contained in:
Kiana Sheibani 2023-10-19 13:52:45 -04:00
parent e362cb9c0e
commit e38d00d4a3
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Control/Lens/Cons.idr
View file

@ -14,7 +14,7 @@ import Control.Lens.Optional
||| left side of a sequence. ||| left side of a sequence.
public export public export
interface Cons s t a b | s where 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)) 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 ||| 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. ||| right side of a sequence.
public export public export
interface Snoc s t a b | s where 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)) 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 ||| This is a prism that can attach or detach a value from the right side of a

2
src/Data/Maybe/Lens.idr
View file

@ -22,7 +22,7 @@ Just_ = prism Just $ \case
infixl 9 .? infixl 9 .?
||| The composition `l .? l'` is equivalent to `l . Just_ . l'`. ||| 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 public export
(.?) : IsPrism p => Optic' p s t (Maybe a) (Maybe b) -> Optic' p a b a' b' -> Optic' p s t a' b' (.?) : 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' l .? l' = l . Just_ . l'