def Lean.Parser.«command__Simproc__[_]_(_):=_» : Lean.ParserDescr

A user-defined simplification procedure used by the simp tactic, and its variants. Here is an example.

simproc reduce_add (_ + _) := fun e => do
  unless (e.isAppOfArity ``HAdd.hAdd 6) do return none
  let some n ← getNatValue? (e.getArg! 4) | return none
  let some m ← getNatValue? (e.getArg! 5) | return none
  return some (.done { expr := mkNatLit (n+m) })

The simp tactic invokes reduce_add whenever it finds a term of the form _ + _. The simplification procedures are stored in an (imperfect) discrimination tree. The procedure should not assume the term e perfectly matches the given pattern. The body of a simplification procedure must have type Simproc, which is an alias for Expr → SimpM (Option Step). You can instruct the simplifier to apply the procedure before its sub-expressions have been simplified by using the modifier ↓ before the procedure name. Example.

simproc ↓ reduce_add (_ + _) := fun e => ...

Simplification procedures can be also scoped or local.

Equations

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

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

A user-defined simplification procedure declaration. To activate this procedure in simp tactic, we must provide it as an argument, or use the command attribute to set its [simproc] attribute.

Equations

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

def Lean.Parser.«command__Builtin_simproc__[_]_(_):=_» : Lean.ParserDescr

A builtin simplification procedure.

Equations

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

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

A builtin simplification procedure declaration.

Equations

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

def Lean.Parser.simprocPattern : Lean.ParserDescr

Auxiliary command for associating a pattern with a simplification procedure.

Equations

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

def Lean.Parser.simprocPatternBuiltin : Lean.ParserDescr

Auxiliary command for associating a pattern with a builtin simplification procedure.

Equations

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

def Lean.Parser.Attr.simprocAttr : Lean.ParserDescr

Auxiliary attribute for simplification procedures.

Equations

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

def Lean.Parser.Attr.sevalprocAttr : Lean.ParserDescr

Auxiliary attribute for symbolic evaluation procedures.

Equations

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

def Lean.Parser.Attr.simprocBuiltinAttr : Lean.ParserDescr

Auxiliary attribute for builtin simplification procedures.

Equations

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

def Lean.Parser.Attr.sevalprocBuiltinAttr : Lean.ParserDescr

Auxiliary attribute for builtin symbolic evaluation procedures.

Equations

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