From 982dcb2e06936ce45438c98863474051d8e1dffb Mon Sep 17 00:00:00 2001 From: Reza Gharibi Date: Thu, 15 Aug 2019 22:46:03 +0430 Subject: [PATCH] Added a missed (practice) label --- src/plfa/part2/Confluence.lagda.md | 2 +- src/plfa/part2/DeBruijn.lagda.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md index ad1f9489..94cd5d7a 100644 --- a/src/plfa/part2/Confluence.lagda.md +++ b/src/plfa/part2/Confluence.lagda.md @@ -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 diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index 94747e8f..beabbdea 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -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