From 104ade010f83c80670ef351a9ae8632fa5c8a20b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Nov 2020 16:22:01 -0800 Subject: [PATCH] chore: weird line break --- src/Lean/Elab/StructInst.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index fa22c7ece8..1095a6a49d 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -25,8 +25,8 @@ open Meta @[builtinMacro Lean.Parser.Term.structInst] def expandStructInstExpectedType : Macro := fun stx => let expectedArg := stx[4] - if expectedArg.isNone - then Macro.throwUnsupported + if expectedArg.isNone then + Macro.throwUnsupported else let expected := expectedArg[1] let stxNew := stx.setArg 4 mkNullNode