From 5d73f0eb01563d7f7b410c71a258c3545e6cbc77 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Dec 2021 15:08:41 -0800 Subject: [PATCH] chore: fix typo --- src/Lean/Elab/PreDefinition/Structural/Eqns.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index d778e65155..0894c863f3 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean @@ -91,7 +91,7 @@ private def simpIf? (mvarId : MVarId) : MetaM (Option MVarId) := do Auxiliary method for `mkEqnTypes`. We should "keep going"/"processing" the goal `... |- f ... = rhs` at `mkEqnTypes` IF `rhs` contains a `f` application containing loose bound variables. We do that to make sure we can create an elimination principle for `f` based - on the generateg equations. + on the generated equations. Remark: we have considered using the same heuristic used in the `BRecOn` module. That is we would do case-analysis on the `match` application because the recursive