feat: add admit tactic

src/Lean/Meta/AppBuilder.lean

@@ -340,5 +340,9 @@ u ← getDecLevel `mkArrayLit type;
 listLit ← mkListLit type xs;
 pure (mkApp (mkApp (mkConst `List.toArray [u]) type) listLit)
 
+def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
+u ← getLevel type;
+pure $ mkApp2 (mkConst `sorryAx [u]) type (toExpr synthetic)
+
 end Meta
 end Lean

src/Lean/Meta/Tactic/Util.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.Basic
+import Lean.Meta.AppBuilder
 import Lean.Meta.LevelDefEq
 
 namespace Lean
@@ -44,5 +45,14 @@ instance Meta.hasOrelse {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩
 @[init] private def regTraceClasses : IO Unit :=
 registerTraceClass `Meta.Tactic
 
+/-- Assign `mvarId` to `sorryAx` -/
+def admit (mvarId : MVarId) (synthetic := true) : MetaM Unit :=
+withMVarContext mvarId $ do
+  checkNotAssigned mvarId `admit;
+  mvarType ← getMVarType mvarId;
+  val ← mkSorry mvarType synthetic;
+  assignExprMVar mvarId val;
+  pure ()
+
 end Meta
 end Lean