def Lean.Parser.cbvSimprocEval : ParserDescr

Equations

• Lean.Parser.cbvSimprocEval = Lean.ParserDescr.nodeWithAntiquot "cbvSimprocEval" `Lean.Parser.cbvSimprocEval (Lean.ParserDescr.symbol "cbv_eval")

def Lean.Parser.«command__Cbv_simproc____(_):=_» : ParserDescr

A user-defined simplification procedure used by the cbv tactic. The body must have type Lean.Meta.Sym.Simp.Simproc (Expr → SimpM Result). Procedures are indexed by a discrimination tree pattern and fire at one of three phases: ↓ (pre), cbv_eval (eval), or ↑ (post, default).

Equations

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

def Lean.Parser.«command_Cbv_simproc_decl_(_):=_» : ParserDescr

A cbv_simproc declaration without automatically adding it to the cbv simproc set. To activate, use attribute [cbv_simproc].

Equations

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

def Lean.Parser.«command__Builtin_cbv_simproc____(_):=_» : ParserDescr

Equations

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

def Lean.Parser.«command_Builtin_cbv_simproc_decl_(_):=_» : ParserDescr

Equations

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

def Lean.Parser.cbvSimprocPattern : ParserDescr

Equations

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

def Lean.Parser.cbvSimprocPatternBuiltin : ParserDescr

Equations

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

def Lean.Parser.Attr.cbvSimprocAttr : ParserDescr

Equations

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

def Lean.Parser.Attr.cbvSimprocBuiltinAttr : ParserDescr

Equations

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