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

fix: use metavariable local context

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-08 18:47:38 -08:00
parent 70bab68dc0
commit 7a556d8f61
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Lean/Meta/Tactic/Util.lean
View file

@ -30,9 +30,8 @@ pure mvarDecl.type
def ppGoal (mvarId : MVarId) : MetaM Format := do
env ← getEnv;
mctx ← getMCtx;
lctx ← getLCtx;
opts ← getOptions;
pure $ ppGoal env mctx lctx opts mvarId
pure $ ppGoal env mctx opts mvarId
@[init] private def regTraceClasses : IO Unit :=
registerTraceClass `Meta.Tactic

3
src/Init/Lean/Util/PPGoal.lean
View file

@ -8,11 +8,12 @@ import Init.Lean.Util.PPExt
namespace Lean
def ppGoal (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (mvarId : MVarId) : Format :=
def ppGoal (env : Environment) (mctx : MetavarContext) (opts : Options) (mvarId : MVarId) : Format :=
match mctx.findDecl? mvarId with
| none => "unknown goal"
| some mvarDecl =>
let indent := 2; -- Use option
let lctx := mvarDecl.lctx;
let pp (e : Expr) : Format := ppExpr env mctx lctx opts e;
let instMVars (e : Expr) : Expr := (mctx.instantiateMVars e).1;
let addLine (fmt : Format) : Format := if fmt.isNil then fmt else fmt ++ Format.line;