opaque FirstOrder.Language.Proof.Tactic.prwExt : Lean.SimpleScopedEnvExtension Lean.Name (Array Lean.Name)

def FirstOrder.Language.Proof.Tactic.prwAttr : Lean.ParserDescr

Congruence theorems tagged with @[prw] attribute are used for prw tactic.

Equations

• FirstOrder.Language.Proof.Tactic.prwAttr = Lean.ParserDescr.node `FirstOrder.Language.Proof.Tactic.prwAttr 1024 (Lean.ParserDescr.nonReservedSymbol "prw" false)