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.
1 parent ee4d349 commit 5d0f79fCopy full SHA for 5d0f79f
src/Data/Fin/Properties.agda
@@ -1054,7 +1054,7 @@ private
1054
¬ (∀ i → P i) → (∃ λ i → ¬ P i)
1055
¬∀⟶∃¬ n P P? ¬P = map id proj₁ (¬∀⟶∃¬-smallest n P P? ¬P)
1056
1057
--- Kleisli lifting of Dec over Unary subset relation
+-- lifting Dec over Unary subset relation
1058
1059
decFinSubset : ∀ {P : Pred (Fin n) p} {Q : Pred (Fin n) q} →
1060
Decidable Q → Q ⊆ Dec ∘ P → Dec (Q ⊆ P)
0 commit comments