Documentation

Lean.Elab.Tactic.Conv.Pattern

source
def Lean.Elab.Tactic.Conv.matchPattern? (pattern : Lean.Meta.AbstractMVarsResult) (e : Lean.Expr) :
Lean.MetaM (Option (Lean.Expr × Array Lean.Expr))
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.Tactic.Conv.matchPattern?.go? (pattern : Lean.Expr) (e : Lean.Expr) :
Lean.MetaM (Option (Lean.Expr × Array Lean.Expr))
source
def Lean.Elab.Tactic.Conv.evalPattern:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.