From: jim Date: Tue, 24 Mar 2015 13:17:23 +0000 (-0400) Subject: ≡ means syntactic identity, not equivalence X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=cabaa3341918874ee26fd368df25383e15b31737;hp=346405d4f6439e7a87409572ba46b84c8628d5c0 ≡ means syntactic identity, not equivalence --- diff --git a/exercises/assignment5_answers.mdwn b/exercises/assignment5_answers.mdwn index 1780b0aa..9be28e21 100644 --- a/exercises/assignment5_answers.mdwn +++ b/exercises/assignment5_answers.mdwn @@ -506,7 +506,7 @@ type `Bool`. also a mistake. What we want is a result whose type _is_ `Bool`, that is, `∀α. α -> α -> α`. `(q [Bool])` doesn't have that type, but rather the type `Bool -> Bool -> Bool`. The first, desired, type has an outermost `∀`. The second, wrong type doesn't; it only has `∀`s inside the antecedents and consequents of the various arrows. The last one of those could be promoted to be an outermost `∀`, since - `P -> ∀α. Q ≡ ∀α. P -> Q` when `α` is not free in `P`. But that couldn't be done with the others. + `P -> ∀α. Q` is equivalent to `∀α. P -> Q` when `α` is not free in `P`. But that couldn't be done with the others. The type `Nat` (for "natural number") may be encoded as follows: