diff options
| author | Iain Lane <laney@ubuntu.com> | 2010-12-10 14:57:42 +0000 |
|---|---|---|
| committer | Iain Lane <laney@ubuntu.com> | 2010-12-10 14:57:42 +0000 |
| commit | cc1f5c802508a4098a9d4ea99c356277cbe5ff0d (patch) | |
| tree | 79907ab1f0044031e018bffe3ed0578fa5176446 /src/Data/Fin/Dec.agda | |
| parent | f294a45d2691b750adc2ed9238db7232aa04ad7b (diff) | |
Imported Upstream version 0.4
Diffstat (limited to 'src/Data/Fin/Dec.agda')
| -rw-r--r-- | src/Data/Fin/Dec.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Data/Fin/Dec.agda b/src/Data/Fin/Dec.agda index 2381131..7b50302 100644 --- a/src/Data/Fin/Dec.agda +++ b/src/Data/Fin/Dec.agda @@ -6,7 +6,7 @@ module Data.Fin.Dec where -open import Data.Function +open import Function open import Data.Nat hiding (_<_) open import Data.Vec hiding (_∈_) open import Data.Fin @@ -40,7 +40,7 @@ private any? : ∀ {n} {P : Fin n → Set} → ((f : Fin n) → Dec (P f)) → Dec (∃ P) -any? {zero} {P} dec = no ((¬ Fin 0 ∶ λ()) ∘ proj₁) +any? {zero} {P} dec = no (((λ()) ∶ ¬ Fin 0) ∘ proj₁) any? {suc n} {P} dec with dec zero | any? (restrict dec) ... | yes p | _ = yes (_ , p) ... | _ | yes (_ , p') = yes (_ , p') |