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

chore: remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-29 14:19:06 -07:00
parent 239a3b9298
commit 26a565496e
1 changed files with 0 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Elab/App.lean
View file

@ -877,13 +877,6 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
trace[Elab.app.args] "explicit: {explicit}, ellipsis: {ellipsis}, {f} : {fType}"
trace[Elab.app.args] "namedArgs: {namedArgs}"
trace[Elab.app.args] "args: {args}"
let go (namedArgs : Array NamedArg) (args : Array Arg) : TermElabM Expr := do
ElabAppArgs.main.run { explicit, ellipsis, resultIsOutParamSupport } |>.run' {
args := args.toList
expectedType?, f, fType
namedArgs := namedArgs.toList
propagateExpected := (← propagateExpectedTypeFor f)
}
if let some elimInfo ← elabAsElim? then
tryPostponeIfNoneOrMVar expectedType?
let some expectedType := expectedType? | throwError "failed to elaborate eliminator, expected type is not available"