@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

Recognizes x1 ≍ x2, returns some (α1, x1, α2, x2).

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

@[inline]

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

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

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

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

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

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

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

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

Recognize α × β

def Lean.Expr.name? : Expr → Option Name

Checks if an expression is a Name literal, and if so returns the name.