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

fix: typo

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-09 16:47:14 -08:00
parent 22ff3c7db2
commit a4a3f7d6a5
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/Init/Lean/Meta/Tactic/Clear.lean
View file

@ -20,7 +20,7 @@ withMVarContext mvarId $ do
lctx.forM $ fun localDecl =>
unless (localDecl.fvarId == fvarId) $
when (mctx.localDeclDependsOn localDecl fvarId) $
throwTacticEx `clear mvarId ("variable '" ++ localDecl.value ++ "' depends on '" ++ mkFVar fvarId ++ "'");
throwTacticEx `clear mvarId ("variable '" ++ localDecl.toExpr ++ "' depends on '" ++ mkFVar fvarId ++ "'");
mvarDecl ← getMVarDecl mvarId;
when (mctx.exprDependsOn mvarDecl.type fvarId) $
throwTacticEx `clear mvarId ("taget depends on '" ++ mkFVar fvarId ++ "'");