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

fix: propagate type before synthesizeSyntheticMVars

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-11 12:01:12 -08:00
parent c729973742
commit 246e0a5532
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Lean/Elab/Definition.lean
View file

@ -83,11 +83,11 @@ withUsedWhen ref vars xs e dummyExpr cond k
def mkDef (view : DefView) (declName : Name) (explictLevelNames : List Name) (vars : Array Expr) (xs : Array Expr) (type : Expr) (val : Expr)
: TermElabM (Option Declaration) := do
let ref := view.ref;
valType ← Term.inferType view.val val;
val ← Term.ensureHasType ref type valType val;
Term.synthesizeSyntheticMVars false;
type ← Term.instantiateMVars ref type;
val ← Term.instantiateMVars view.val val;
valType ← Term.inferType view.val val;
val ← Term.ensureHasType ref type valType val;
if view.kind.isExample then pure none
else withUsedWhen ref vars xs val type view.kind.isDefOrOpaque $ fun vars => do
type ← Term.mkForall ref xs type;

2
tests/lean/run/termParserAttr.lean
View file

@ -63,7 +63,7 @@ def fooParser (rbp : Nat := 0) : Parser := categoryParser (mkNameSimple "foo") r
@[termParser] def tst3 := parser! symbol "FOO " 0 >> fooParser 0
@[termElab tst3] def elabTst3 : TermElab :=
fun (stx : Syntax) expected? =>
fun stx expected? =>
elabTerm ((stx.getArg 1).getArg 1) expected?
#check FOO ⟨| id 1 |⟩