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

fix: new type ascription elaborator

Browse source 
It was propating the incorrect type.
This commit is contained in:
Leonardo de Moura 2021-04-27 16:03:27 -07:00
parent 2e250e6f04
commit e8531ef4de
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/BuiltinNotation.lean
View file

@ -230,7 +230,7 @@ where
match ← expandCDot? e with
| some e => `(($e : $type))
| none => Macro.throwUnsupported
| `(($e)) => do return (← expandCDot? e).getD e
| `(($e)) => return (← expandCDot? e).getD e
| `(($e, $es,*)) => do
let pairs ← mkPairs (#[e] ++ es)
(← expandCDot? pairs).getD pairs
@ -240,7 +240,7 @@ where
match stx with
| `(($e : $type)) =>
let type ← withSynthesize (mayPostpone := true) <| elabType type
let e ← elabTerm e expectedType?
let e ← elabTerm e type
ensureHasType type e
| _ => throwUnsupportedSyntax