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

chore: fix docstring

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-07 07:13:32 -08:00
parent 2753822fe7
commit 6d236fbf2e
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/Meta/ExprDefEq.lean
View file

@ -107,7 +107,7 @@ def isEtaUnassignedMVar (e : Expr) : MetaM Bool := do
```
fun x₁ ... xₙ => ?m x₁ ... xₙ =?= t
t =?= fun x₁ ... xₙ => ?m x₁ ... xₙ
```
This is important because type inference often produces
eta-expanded terms, and without this extra case, we could
introduce counter intuitive behavior.