We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
Data.List.Relation.Unary.Any.Properties
1 parent 0409790 commit f831cb2Copy full SHA for f831cb2
src/Data/List/Relation/Unary/Any/Properties.agda
@@ -102,7 +102,7 @@ module _ {k : Kind} {P : Pred A p} {Q : Pred A q} where
102
where open Related.EquationalReasoning
103
104
------------------------------------------------------------------------
105
--- map
+-- Any.map
106
107
map-id : ∀ {P : A → Set p} (f : P ⋐ P) {xs} →
108
(∀ {x} (p : P x) → f p ≡ p) →
@@ -118,7 +118,7 @@ map-∘ f g (here p) = refl
118
map-∘ f g (there p) = P.cong there $ map-∘ f g p
119
120
121
--- lookup
+-- Any.lookup
122
123
lookup-result : ∀ {P : Pred A p} {xs} → (p : Any P xs) → P (Any.lookup p)
124
lookup-result (here px) = px
0 commit comments