This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module FilterProof where | |
| open import Data.List hiding (filter; concat) | |
| open import Data.Bool | |
| import Relation.Binary.PropositionalEquality as Eq | |
| open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst) | |
| open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎) | |
| private variable | |
| A : Set | |
| B : Set |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module LEM where | |
| open import Data.Nat | |
| open import Data.Bool | |
| open import Relation.Nullary using (¬_) | |
| open import Data.Sum using (inj₁; inj₂) renaming (_⊎_ to _∨_) | |
| open import Relation.Nullary using (Dec; yes; no) | |
| -- A predicate about if nat is even. | |
| data Even : ℕ → Set where |