ink

def Lean.Parser.Tactic.simpArg : Lean.ParserDescr

A simpArg is either a *, -lemma or a simp lemma specification (which includes the ↑↑ ↓↓ ←← specifications for pre, post, reverse rewriting).

Equations

• Lean.Parser.Tactic.simpArg = Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.simpStar (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.simpErase Lean.Parser.Tactic.simpLemma)

ink

def Lean.Parser.Tactic.simpArgs : Lean.ParserDescr

A simp args list is a list of simpArg. This is the main argument to simp.

Equations

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

ink

def Lean.Parser.Tactic.getSimpArgs? : Lean.Syntax → Option (Array Lean.Syntax)

Extract the arguments from a simpArgs syntax as an array of syntaxes

Equations

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

ink

def Lean.Parser.Tactic.dsimpArg : Lean.ParserDescr

A dsimpArg is similar to simpArg, but it does not have the simpStar form because it does not make sense to use hypotheses in dsimp.

Equations

• Lean.Parser.Tactic.dsimpArg = Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.simpErase Lean.Parser.Tactic.simpLemma

ink

def Lean.Parser.Tactic.dsimpArgs : Lean.ParserDescr

A dsimp args list is a list of dsimpArg. This is the main argument to dsimp.

Equations

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

ink

def Lean.Parser.Tactic.getDSimpArgs? : Lean.Syntax → Option (Array Lean.Syntax)

Extract the arguments from a dsimpArgs syntax as an array of syntaxes

Equations

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