def Lean.Elab.Tactic.Do.ProofMode.mSpecializeImpStateful (σs P QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.ProofMode.mSpecializeImpPure (_σs P QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.ProofMode.mSpecializeForall (_σs P Ψ : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.ProofMode.elabMSpecialize : Tactic

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.ProofMode.elabMspecializePure : Tactic

Equations

• One or more equations did not get rendered due to their size.