Skip to content

Instantly share code, notes, and snippets.

Avatar

Mauricio Collares collares

View GitHub Profile
View Lists.agda
module plfa.Lists where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax)
renaming (_,_ to ⟨_,_⟩)
open import plfa.Isomorphism using (_≃_)
data List (A : Set) : Set where
[] : List A
View Minimized.agda
module plfa.Minimized where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open import Function using (_∘_)
open import Data.List using (List; []; _∷_)
open import Data.List.All using (All; []; _∷_)
open import Data.List.Any using (Any; here; there)
open import Data.List.Membership.Propositional using (_∈_)
open import Relation.Nullary using (¬_)
View Minimized.agda
module plfa.Minimized where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Function using (_∘_)
data _×_ (A B : Set) : Set where
⟨_,_⟩ : A B A × B
proj₁ : {A B : Set} A × B A