michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

added proj_2 to imports in Qualifiers

Browse source
This commit is contained in:
wadler 2020-04-17 12:14:55 -03:00
parent 6d97cb0101
commit 29157501d4
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/part1/Quantifiers.lagda.md
View file

@ -19,7 +19,7 @@ import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl) open Eq using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_) open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Relation.Nullary using (¬_) open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; proj₁) renaming (_,_ to ⟨_,_⟩) open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_) open import Data.Sum using (_⊎_)
open import plfa.part1.Isomorphism using (_≃_; extensionality) open import plfa.part1.Isomorphism using (_≃_; extensionality)
``` ```