From edc655340e38cfee80d2b1bf882254940b7ffee9 Mon Sep 17 00:00:00 2001 From: Owen Shepherd Date: Fri, 26 Dec 2025 17:42:49 +0000 Subject: [PATCH] Remove stray 'either' with no else-clause This `either a or b` seems to be missing an `or b`. I'm also wondering about the `fun-expressions` wording. Does this mean that definitional equality doesn't apply to functions defined with `def`? --- book/FPLean/DependentTypes/Pitfalls.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/FPLean/DependentTypes/Pitfalls.lean b/book/FPLean/DependentTypes/Pitfalls.lean index 33a745a..1a42ec9 100644 --- a/book/FPLean/DependentTypes/Pitfalls.lean +++ b/book/FPLean/DependentTypes/Pitfalls.lean @@ -172,7 +172,7 @@ They also contain _variables_ and _functions_. Definitional equality of variables is relatively simple: each variable is equal only to itself, so {anchorTerm moreNames}`(n k : Nat) → Vect Int n` is not definitionally equal to {anchorTerm moreNames}`(n k : Nat) → Vect Int k`. Functions, on the other hand, are more complicated. While mathematics considers two functions to be equal if they have identical input-output behavior, there is no efficient algorithm to check that, and the whole point of definitional equality is for Lean to check whether two types are interchangeable. -Instead, Lean considers functions to be definitionally equal either when they are both {kw}`fun`-expressions with definitionally equal bodies. +Instead, Lean considers functions to be definitionally equal when they are both {kw}`fun`-expressions with definitionally equal bodies. In other words, two functions must use _the same algorithm_ that calls _the same helpers_ to be considered definitionally equal. This is not typically very helpful, so definitional equality of functions is mostly used when the exact same defined function occurs in two types.