max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix typo

Browse source
This commit is contained in:
Leonardo de Moura 2021-12-01 15:08:41 -08:00
parent c54caa1a1f
commit 5d73f0eb01
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/PreDefinition/Structural/Eqns.lean
View file

@ -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