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

minor update to Naturals

Browse source
This commit is contained in:
wadler 2018-05-26 12:22:30 -03:00
parent 83a62f55d9
commit adc4d3abb2
2 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Connectives.lagda
View file

@ -770,11 +770,12 @@ embedding, revealing a sense in which one of these laws is "more
true" than the other. true" than the other.
### Exercise (`×⊎-implies-⊎×`) ### Exercise (`⊎×-implies-×⊎`)
Show that a conjunct of disjuncts implies a disjunct of conjuncts. Show that a disjunct of conjuncts implies a conjunct of disjuncts.
\begin{code} \begin{code}
×⊎-Implies-⊎× = ∀ {A B C D : Set} → (A ⊎ B) × (C ⊎ D) → (A × C) ⊎ (B × D) postulate
⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
\end{code} \end{code}
Does the converse hold? If so, prove; if not, explain why. Does the converse hold? If so, prove; if not, explain why.

4
src/Naturals.lagda
View file

@ -82,8 +82,8 @@ zero or more *judgments* written above a horizontal line, called the
*conclusion*. The first rule is the base case. It has no hypotheses, *conclusion*. The first rule is the base case. It has no hypotheses,
and the conclusion asserts that `zero` is a natural. The second rule and the conclusion asserts that `zero` is a natural. The second rule
is the inductive case. It has one hypothesis, which assumes that `m` is the inductive case. It has one hypothesis, which assumes that `m`
is a natural, and the conclusion asserts that `suc n` is a also a is a natural, and in that case the conclusion asserts that `suc n`
natural. is a also a natural.
## Unpacking the Agda definition ## Unpacking the Agda definition