def Lean.Parser.cbvSimprocEval : ParserDescr

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).

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].

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

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

def Lean.Parser.cbvSimprocPattern : ParserDescr

def Lean.Parser.cbvSimprocPatternBuiltin : ParserDescr

def Lean.Parser.Attr.cbvSimprocAttr : ParserDescr

def Lean.Parser.Attr.cbvSimprocBuiltinAttr : ParserDescr