This directory contains the syntax definition for tactics related to the proof mode of Std.Do.SPred. Their builtin implementation lives in Lean.Elab.Tactic.Do to enable using the tactics without public importing Lean.