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

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

theorem and_false_eq {p : Prop} (q : Prop) (h : p = False) : (p ∧ q) = False := by simp [*]

open Lean Meta Simp
simproc ↓ shortCircuitAnd (And _ _) := fun e => do
  let_expr And p q := e | return .continue
  let r ← simp p
  let_expr False := r.expr | return .continue
  let proof ← mkAppM ``and_false_eq #[q, (← r.getProof)]
  return .done { expr := r.expr, proof? := some proof }

The simp tactic invokes shortCircuitAnd whenever it finds a term of the form And _ _. 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 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. Simplification procedures can be also scoped or local.

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

Similar to simproc, but resulting expression must be definitionally equal to the input one.

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.

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

A user-defined defeq 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.

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_dsimproc__[_]_(_):=_» : Lean.ParserDescr

A builtin defeq simplification procedure.

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.«command_Builtin_dsimproc_decl_(_):=_» : Lean.ParserDescr

A builtin defeq simplification procedure declaration.

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.

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.

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.