@[inline]

def Lean.Expr.const? (e : Lean.Expr) : Option (Lake.Name × List Lean.Level)

@[inline]

def Lean.Expr.app1? (e : Lean.Expr) (fName : Lake.Name) : Option Lean.Expr

@[inline]

def Lean.Expr.app2? (e : Lean.Expr) (fName : Lake.Name) : Option (Lean.Expr × Lean.Expr)

@[inline]

def Lean.Expr.app3? (e : Lean.Expr) (fName : Lake.Name) : Option (Lean.Expr × Lean.Expr × Lean.Expr)

@[inline]

def Lean.Expr.app4? (e : Lean.Expr) (fName : Lake.Name) : Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)

@[inline]

def Lean.Expr.eq? (p : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr)

@[inline]

def Lean.Expr.ne? (p : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr)

@[inline]

def Lean.Expr.iff? (p : Lean.Expr) : Option (Lean.Expr × Lean.Expr)

@[inline]

def Lean.Expr.eqOrIff? (p : Lean.Expr) : Option (Lean.Expr × Lean.Expr)

@[inline]

def Lean.Expr.not? (p : Lean.Expr) : Option Lean.Expr

@[inline]

def Lean.Expr.notNot? (p : Lean.Expr) : Option Lean.Expr

@[inline]

def Lean.Expr.and? (p : Lean.Expr) : Option (Lean.Expr × Lean.Expr)

@[inline]

def Lean.Expr.heq? (p : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)

def Lean.Expr.natAdd? (e : Lean.Expr) : Option (Lean.Expr × Lean.Expr)

@[inline]

def Lean.Expr.arrow? : Lean.Expr → Option (Lean.Expr × Lean.Expr)

def Lean.Expr.isEq (e : Lean.Expr) : Bool

def Lean.Expr.isHEq (e : Lean.Expr) : Bool

def Lean.Expr.isIte (e : Lean.Expr) : Bool

def Lean.Expr.isDIte (e : Lean.Expr) : Bool

def Lean.Expr.listLit? (e : Lean.Expr) : Option (Lean.Expr × List Lean.Expr)

partial def Lean.Expr.listLit?.loop (e : Lean.Expr) (acc : List Lean.Expr) : Option (Lean.Expr × List Lean.Expr)

def Lean.Expr.arrayLit? (e : Lean.Expr) : Option (Lean.Expr × List Lean.Expr)

def Lean.Expr.prod? (e : Lean.Expr) : Option (Lean.Expr × Lean.Expr)

Recognize α × β

def Lean.Expr.isConstructorApp? (env : Lean.Environment) (e : Lean.Expr) : Option Lean.ConstructorVal

def Lean.Expr.isConstructorApp (env : Lean.Environment) (e : Lean.Expr) : Bool

def Lean.Expr.constructorApp? (env : Lean.Environment) (e : Lean.Expr) (useRaw : optParam Bool false) : Option (Lean.ConstructorVal × Array Lean.Expr)

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).