From d3da0abc8a5116d1a2c2da5cee56b44091d25d77 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Dec 2019 10:21:20 -0800 Subject: [PATCH] chore: style --- src/Init/Lean/Elab/Term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index 1a8c62707e..332f1036ee 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -125,7 +125,7 @@ def getCurrNamespace : TermElabM Name := do ctx ← read; pure ctx.currNamespace def getOpenDecls : TermElabM (List OpenDecl) := do ctx ← read; pure ctx.openDecls def getLCtx : TermElabM LocalContext := do ctx ← read; pure ctx.lctx def getLocalInsts : TermElabM LocalInstances := do ctx ← read; pure ctx.localInstances -def getOptions : TermElabM Options := do ctx ← read; pure ctx.config.opts +def getOptions : TermElabM Options := do ctx ← read; pure ctx.config.opts def getTraceState : TermElabM TraceState := do s ← get; pure s.traceState def setTraceState (traceState : TraceState) : TermElabM Unit := modify $ fun s => { traceState := traceState, .. s } def isExprMVarAssigned (mvarId : MVarId) : TermElabM Bool := do mctx ← getMCtx; pure $ mctx.isExprAssigned mvarId