feat: add evalClear

src/Init/Lean/Elab/Tactic/Basic.lean

@@ -7,6 +7,8 @@ prelude
 import Init.Lean.Util.CollectMVars
 import Init.Lean.Meta.Tactic.Assumption
 import Init.Lean.Meta.Tactic.Intro
+import Init.Lean.Meta.Tactic.Clear
+import Init.Lean.Meta.Tactic.Revert
 import Init.Lean.Elab.Util
 import Init.Lean.Elab.Term
 
@@ -344,6 +346,20 @@ fun stx => match_syntax stx with
        setGoals (g :: gs)
   | _                     => throwUnsupportedSyntax
 
+@[builtinTactic «clear»] def evalClear : Tactic :=
+fun stx => match_syntax stx with
+  | `(tactic| clear $hs*) =>
+    hs.forM $ fun h => do
+      (g, gs) ← getMainGoal stx;
+      withMVarContext g $ do
+        fvar? ← liftTermElabM $ Term.isLocalTermId? h true;
+        match fvar? with
+        | none      => throwError h ("unknown variable '" ++ toString h.getId ++ "'")
+        | some fvar => do
+          g ← liftMetaM stx $ Meta.clear g fvar.fvarId!;
+          setGoals (g :: gs)
+  | _                     => throwUnsupportedSyntax
+
 @[builtinTactic paren] def evalParen : Tactic :=
 fun stx => evalTactic (stx.getArg 1)
 

src/Init/Lean/Meta/Tactic/Clear.lean

@@ -14,13 +14,13 @@ withMVarContext mvarId $ do
   checkNotAssigned mvarId `clear;
   lctx ← getLCtx;
   unless (lctx.contains fvarId) $
-    throwTacticEx `clear mvarId ("unknown hypothesis '" ++ mkFVar fvarId ++ "'");
+    throwTacticEx `clear mvarId ("unknown variable '" ++ mkFVar fvarId ++ "'");
   tag ← getMVarTag mvarId;
   mctx ← getMCtx;
   lctx.forM $ fun localDecl =>
     unless (localDecl.fvarId == fvarId) $
       when (mctx.localDeclDependsOn localDecl fvarId) $
-        throwTacticEx `clear mvarId ("hypothesis '" ++ localDecl.value ++ "' depends on '" ++ mkFVar fvarId ++ "'");
+        throwTacticEx `clear mvarId ("variable '" ++ localDecl.value ++ "' depends on '" ++ mkFVar fvarId ++ "'");
   mvarDecl ← getMVarDecl mvarId;
   when (mctx.exprDependsOn mvarDecl.type fvarId) $
     throwTacticEx `clear mvarId ("taget depends on '" ++ mkFVar fvarId ++ "'");

tests/lean/run/newfrontend1.lean

@@ -185,6 +185,17 @@ begin
   exact h1
 end
 
+theorem simple16 (x y z : Nat) : y = z → x = x → x = y → x = z :=
+begin
+  intros h1 h2 h3;
+  -- clear x;
+  clear h2;
+  traceState;
+  apply Eq.trans;
+  exact h3;
+  exact h1
+end
+
 macro "blabla" : tactic => `(assumption)
 
 -- Tactic head symbols do not become reserved words
@@ -192,7 +203,7 @@ def blabla := 100
 
 #check blabla
 
-theorem simple16 (x : Nat) (h : x = 0) : x = 0 :=
+theorem simple17 (x : Nat) (h : x = 0) : x = 0 :=
 begin blabla end
 
 theorem tstprec1 (x y z : Nat) : x + y * z = x + (y * z) :=