diff options
| author | Gianfranco Costamagna <costamagnagianfranco@yahoo.it> | 2017-11-26 11:35:06 +0100 |
|---|---|---|
| committer | Gianfranco Costamagna <costamagnagianfranco@yahoo.it> | 2017-11-26 11:35:06 +0100 |
| commit | 0b3946998d82e1be6c50e2872e7474db69b5a0dc (patch) | |
| tree | c935ec365b32a5d11dddea90cc53aa9e7ad9bf3c /src/Data/Fin/Dec.agda | |
| parent | c7745ec5e54ac1945fe7161ee9d6e47b10cc59bd (diff) | |
New upstream version 0.14
Diffstat (limited to 'src/Data/Fin/Dec.agda')
| -rw-r--r-- | src/Data/Fin/Dec.agda | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Data/Fin/Dec.agda b/src/Data/Fin/Dec.agda index ef3747d..2a31707 100644 --- a/src/Data/Fin/Dec.agda +++ b/src/Data/Fin/Dec.agda @@ -155,6 +155,14 @@ anySubset? {suc n} {P} dec with anySubset? (restrictS inside dec) extend′ g zero = P0 extend′ g (suc j) = g j + +-- When P is a decidable predicate over a finite set the following +-- lemma can be proved. + +¬∀⟶∃¬ : ∀ n {p} (P : Fin n → Set p) → U.Decidable P → + ¬ (∀ i → P i) → ∃ λ i → ¬ P i +¬∀⟶∃¬ n P dec ¬P = Prod.map id proj₁ $ ¬∀⟶∃¬-smallest n P dec ¬P + -- Decision procedure for _⊆_ (obtained via the natural lattice -- order). |