# Documentation

Lean.Util.Recognizers

@[inline]
Equations
• = match e with | => some (n, us) | x => none
@[inline]
def Lean.Expr.app1? (e : Lean.Expr) (fName : Lean.Name) :
Equations
@[inline]
def Lean.Expr.app2? (e : Lean.Expr) (fName : Lean.Name) :
Equations
@[inline]
def Lean.Expr.app3? (e : Lean.Expr) (fName : Lean.Name) :
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.Expr.app4? (e : Lean.Expr) (fName : Lean.Name) :
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
• = match with | some p => | none => none
@[inline]
Equations
@[inline]
Equations
Equations
@[inline]
Equations
• = match x with | Lean.Expr.forallE binderName α β binderInfo => if then none else some (α, β) | x => none
Equations
Equations
partial def Lean.Expr.listLit?.loop (e : Lean.Expr) (acc : ) :
Equations

Recognize α × β× β

Equations
Equations
• One or more equations did not get rendered due to their size.
def Lean.Expr.constructorApp? (env : Lean.Environment) (e : Lean.Expr) (useRaw : ) :

If e is a constructor application, return a pair containing the corresponding ConstructorVal and the constructor application arguments. This function treats numerals as constructors. For example, if e is the numeral 2, the result pair is ConstructorVal for Nat.succ, and the array #[1]. The parameter useRaw controls how the resulting numeral is represented. If useRaw := false, then mkNatLit is used, otherwise mkRawNatLit. Recall that mkNatLit uses the OfNat.ofNat application which is the canonical way of representing numerals in the elaborator and tactic framework. We useRaw := false in the compiler (aka code generator).

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