From 6e7d76f4d85c3f121d70c7f04f3701c449be6972 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 3 Feb 2022 17:12:27 -0500 Subject: [PATCH] fix: typo --- src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean | 6 +++--- src/Lean/Meta/WHNF.lean | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean index 32d7c098e1..aab5ba1195 100644 --- a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean +++ b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean @@ -17,12 +17,12 @@ partial def addSmartUnfoldingDefAux (preDef : PreDefinition) (recArgPos : Nat) : } where /-- - Auxiliary method for annotating `match`-alternatives with `markSmartUnfoldingMatch` and `markSmartUnfoldigMatchAlt`. + Auxiliary method for annotating `match`-alternatives with `markSmartUnfoldingMatch` and `markSmartUnfoldingMatchAlt`. It uses the following approach: - Whenever it finds a `match` application `e` s.t. `recArgHasLooseBVarsAt preDef.declName recArgPos e`, it marks the `match` with `markSmartUnfoldingMatch`, and each alternative that does not contain a nested marked `match` - is marked with `markSmartUnfoldigMatchAlt`. + is marked with `markSmartUnfoldingMatchAlt`. Recall that the condition `recArgHasLooseBVarsAt preDef.declName recArgPos e` is the one used at `mkBRecOn`. -/ @@ -52,7 +52,7 @@ where let containsSUnfoldMatch := Option.isSome <| altBody.find? fun e => smartUnfoldingMatch? e |>.isSome if !containsSUnfoldMatch then let altBody ← mkLambdaFVars xs[numParams:xs.size] altBody - let altBody := markSmartUnfoldigMatchAlt altBody + let altBody := markSmartUnfoldingMatchAlt altBody mkLambdaFVars xs[0:numParams] altBody else mkLambdaFVars xs altBody diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 35ab03baa8..966ca2c47a 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -39,7 +39,7 @@ def smartUnfoldingMatch? (e : Expr) : Option Expr := annotation? `sunfoldMatch e /-- Add auxiliary annotation to indicate expression `e` (a `match` alternative rhs) was successfully reduced by smart unfolding. -/ -def markSmartUnfoldigMatchAlt (e : Expr) : Expr := +def markSmartUnfoldingMatchAlt (e : Expr) : Expr := mkAnnotation `sunfoldMatchAlt e def smartUnfoldingMatchAlt? (e : Expr) : Option Expr := @@ -472,7 +472,7 @@ partial def whnfCore (e : Expr) : MetaM Expr := | _ => unreachable! /-- - Recall that `_sunfold` auxiliary definitions contains the markers: `markSmartUnfoldigMatch` (*) and `markSmartUnfoldigMatchAlt` (**). + Recall that `_sunfold` auxiliary definitions contains the markers: `markSmartUnfoldingMatch` (*) and `markSmartUnfoldingMatchAlt` (**). For example, consider the following definition ``` def r (i j : Nat) : Nat := @@ -496,7 +496,7 @@ partial def whnfCore (e : Expr) : MetaM Expr := | Nat.succ j => (**) r i j ``` - `match` expressions marked with `markSmartUnfoldigMatch` (*) must be reduced, otherwise the resulting term is not definitionally + `match` expressions marked with `markSmartUnfoldingMatch` (*) must be reduced, otherwise the resulting term is not definitionally equal to the given expression. The recursion may be interrupted as soon as the annotation `markSmartUnfoldingAlt` (**) is reached. For example, the term `r i j.succ.succ` reduces to the definitionally equal term `i + i * r i j`