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

feat: postpone only if inferred type is unknown and there are arguments

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-12 12:26:24 -08:00
parent 7cd0e0a7a5
commit e35f79feb5
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Lean/Elab/App.lean
View file

@ -271,7 +271,8 @@ private def elabAppArgs (ref : Syntax) (f : Expr) (namedArgs : Array NamedArg) (
fType ← inferType ref f;
fType ← instantiateMVars ref fType;
trace `Elab.app.args ref $ fun _ => "explicit: " ++ toString explicit ++ ", " ++ f ++ " : " ++ fType;
tryPostponeIfMVar fType;
unless (namedArgs.isEmpty && args.isEmpty) $
tryPostponeIfMVar fType;
elabAppArgsAux {ref := ref, args := args, expectedType? := expectedType?, explicit := explicit, namedArgs := namedArgs } f fType
/-- Auxiliary inductive datatype that represents the resolution of an `LVal`. -/