Added a missed (practice) label
This commit is contained in:
parent
8f27869beb
commit
982dcb2e06
2 changed files with 2 additions and 2 deletions
|
@ -488,7 +488,7 @@ The proof is by induction on both premises.
|
|||
and `(ƛ N₂) · M₂ ⇛ N₃ [ M₃ ]`
|
||||
by rule `pbeta`
|
||||
|
||||
#### Exercise
|
||||
#### Exercise (practice)
|
||||
|
||||
Draw pictures that represent the proofs of each of the six cases in
|
||||
the above proof of `par-diamond`. The pictures should consist of nodes
|
||||
|
|
|
@ -479,7 +479,7 @@ contexts. While we are at it, we also generalise `twoᶜ` and
|
|||
|
||||
|
||||
|
||||
#### Exercise (`mul`) (recommended)
|
||||
#### Exercise `mul` (recommended)
|
||||
|
||||
Write out the definition of a lambda term that multiplies
|
||||
two natural numbers, now adapted to the inherently typed
|
||||
|
|
Loading…
Reference in a new issue