From 49bdbf7eb25b8a92dad1344e143fdaff8eb2442a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Dec 2019 08:43:17 -0800 Subject: [PATCH] chore: style --- src/Init/Lean/Elab/TermApp.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/TermApp.lean index dd401e6961..51fd8a17a3 100644 --- a/src/Init/Lean/Elab/TermApp.lean +++ b/src/Init/Lean/Elab/TermApp.lean @@ -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