From ba3d6103fa3a2bb5e501da0542cd41cf50785151 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 27 Mar 2021 14:07:45 -0700 Subject: [PATCH] chore: spaces --- src/Lean/LocalContext.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index c931345744..9defcfc226 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -283,9 +283,9 @@ variable {β : Type u} | some decl => f decl instance : ForIn m LocalContext LocalDecl where - forIn lctx init f := lctx.decls.forIn init fun d? b => match d? with + forIn lctx init f := lctx.decls.forIn init fun d? b => match d? with | none => ForInStep.yield b - | some d => f d b + | some d => f d b end