Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2022 Evan Lohn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Evan Lohn, Mario Carneiro
-/
import Lean

namespace Mathlib.Tactic.Substs
open Lean Meta Elab
open Tactic

/--
Applies the `subst` tactic to all given hypotheses from left to right.
-/
syntax (name := 
substs: ParserDescr
substs) "substs" (
colGt: optParam String "checkColGt" → Parser.Parser
colGt 
ppSpace: Parser.Parser
ppSpace 
ident: Parser.Parser
ident)* : 
tactic: Parser.Category
tactic

macro_rules
| `(tactic| substs $
xs: ?m.90
xs:ident*) => `(tactic| ($[subst $
xs: ?m.388
xs]*))