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

small cleanup to standard library

Browse source
This commit is contained in:
wadler 2017-06-20 15:16:50 +01:00
parent ab6da37b16
commit f5fca1e270
1 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Maps.lagda
View file

@ -27,20 +27,19 @@ Unlike the chapters we have seen so far, this one does not
import the chapter before it (and, transitively, all the import the chapter before it (and, transitively, all the
earlier chapters). Instead, in this chapter and from now, on earlier chapters). Instead, in this chapter and from now, on
we're going to import the definitions and theorems we need we're going to import the definitions and theorems we need
directly from Agda's standard library stuff. You should not notice directly from Agda's standard library. You should not notice
much difference, though, because we've been careful to name our much difference, though, because we've been careful to name our
own definitions and theorems the same as their counterparts in the own definitions and theorems the same as their counterparts in the
standard library, wherever they overlap. standard library, wherever they overlap.
\begin{code} \begin{code}
open import Function using (_∘_)
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ) open import Data.Nat using (ℕ)
open import Data.Empty using (⊥; ⊥-elim) open import Data.Empty using (⊥; ⊥-elim)
open import Data.Maybe using (Maybe; just; nothing) open import Data.Maybe using (Maybe; just; nothing)
open import Data.String using (String) open import Data.String using (String)
open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality open import Relation.Binary.PropositionalEquality
using (_≡_; refl; _≢_; trans; sym)
\end{code} \end{code}
Documentation for the standard library can be found at Documentation for the standard library can be found at
@ -293,9 +292,9 @@ updates.
→ x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z → x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
update-permute′ {A} ρ x v y w z x≢y with x ≟ z | y ≟ z update-permute′ {A} ρ x v y w z x≢y with x ≟ z | y ≟ z
... | yes x≡z | yes y≡z = ⊥-elim (x≢y (trans x≡z (sym y≡z))) ... | yes x≡z | yes y≡z = ⊥-elim (x≢y (trans x≡z (sym y≡z)))
... | no x≢z | yes y≡z rewrite y≡z = {!!} -- sym (update-eq′ ρ z w) ... | no x≢z | yes y≡z rewrite y≡z = {! sym (update-eq′ ρ z w)!}
... | yes x≡z | no y≢z rewrite x≡z = {!!} -- update-eq′ ρ z v ... | yes x≡z | no y≢z rewrite x≡z = {! update-eq′ ρ z v!}
... | no x≢z | no y≢z = {!!} -- trans (update-neq ρ y w z y≢z) (sym (update-neq ρ x v z x≢z)) ... | no x≢z | no y≢z = {! trans (update-neq ρ y w z y≢z) (sym (update-neq ρ x v z x≢z))!}
{- {-
Holes are typed as follows. What do the "| z ≟ z" mean, and how can I deal with them? Holes are typed as follows. What do the "| z ≟ z" mean, and how can I deal with them?