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

chore: missing ) in trace message

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-30 20:20:57 -08:00
parent a32c45a515
commit bdd0eae625
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/Subst.lean
View file

@ -29,7 +29,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
match a with
| Expr.fvar aFVarId _ => do
let aFVarIdOriginal := aFVarId
trace[Meta.Tactic.subst]! "substituting {a} (id: {aFVarId} with {b}"
trace[Meta.Tactic.subst]! "substituting {a} (id: {aFVarId}) with {b}"
let mctx ← getMCtx
if mctx.exprDependsOn b aFVarId then
throwTacticEx `subst mvarId m!"'{a}' occurs at{indentExpr b}"