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

updated Agda

Browse source
This commit is contained in:
wadler 2018-02-08 14:31:35 -04:00
parent 2e93d44877
commit 2871611bec
2 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Equivalence.lagda
View file

@ -281,11 +281,10 @@ that `even (n + m)` holds.
Agda includes special notation to support just this Agda includes special notation to support just this
kind of reasoning. To enable this notation, we use kind of reasoning. To enable this notation, we use
pragmas to tell Agda which types and constructors pragmas to tell Agda which type
correspond to equivalence and refl. corresponds to equivalence.
\begin{code} \begin{code}
{-# BUILTIN EQUALITY _≡_ #-} {-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}
\end{code} \end{code}
We can then prove the desired property as follows. We can then prove the desired property as follows.

3
src/Lists.lagda
View file

@ -14,7 +14,6 @@ import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong) open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_) open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties.Simple using (distribʳ-*-+; *-comm)
\end{code} \end{code}
## Lists ## Lists
@ -72,8 +71,6 @@ of `List A` by `List ℕ`, say.
Including the lines Including the lines
\begin{code} \begin{code}
{-# BUILTIN LIST List #-} {-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _∷_ #-}
\end{code} \end{code}
tells Agda that the type `List` corresponds to the Haskell type tells Agda that the type `List` corresponds to the Haskell type
list, and the constructors `[]` and `_∷_` correspond to nil and list, and the constructors `[]` and `_∷_` correspond to nil and