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

fix: missing do

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-24 19:40:40 -07:00
parent cf734814fd
commit 2ff8052ce4
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/BuiltinNotation.lean
View file

@ -255,7 +255,7 @@ where
| some (α, lhs, rhs) =>
let mut lhs := lhs
let mut rhs := rhs
let mkMotive (typeWithLooseBVar : Expr) :=
let mkMotive (typeWithLooseBVar : Expr) := do
withLocalDeclD (← mkFreshUserName `x) α fun x => do
mkLambdaFVars #[x] $ typeWithLooseBVar.instantiate1 x
let mut expectedAbst ← kabstract expectedType rhs