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

chore: style

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-19 08:43:17 -08:00
parent 6eeb64bf88
commit 49bdbf7eb2
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/Init/Lean/Elab/TermApp.lean
View file

@ -234,7 +234,7 @@ private def addLValArg (ref : Syntax) (baseName : Name) (fullName : Name) (e : E
private def elabAppLValsAux (ref : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit : Bool)
: Expr → List LVal → TermElabM Expr
| f, [] => elabAppArgs ref f namedArgs args expectedType? explicit
| f, [] => elabAppArgs ref f namedArgs args expectedType? explicit
| f, lval::lvals => do
lvalRes ← resolveLVal ref f lval;
match lvalRes with