@[inline]

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

Equations

• (Lean.Expr.const n us).const? = some (n, us)
• e.const? = none

@[inline]

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

Equations

• e.app1? fName = if e.isAppOfArity fName 1 = true then some e.appArg! else none

@[inline]

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

Equations

• e.app2? fName = if e.isAppOfArity fName 2 = true then some (e.appFn!.appArg!, e.appArg!) else none

@[inline]

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

Equations

• e.app3? fName = if e.isAppOfArity fName 3 = true then some (e.appFn!.appFn!.appArg!, e.appFn!.appArg!, e.appArg!) else none

@[inline]

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

Equations

• e.app4? fName = if e.isAppOfArity fName 4 = true then some (e.appFn!.appFn!.appFn!.appArg!, e.appFn!.appFn!.appArg!, e.appFn!.appArg!, e.appArg!) else none

@[inline]

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

Equations

• p.eq? = p.app3? `Eq

@[inline]

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

Equations

• p.ne? = p.app3? `Ne

@[inline]

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

Equations

• p.iff? = p.app2? `Iff

@[inline]

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

Equations

• p.eqOrIff? = match p.app3? `Eq with | some (fst, lhs, rhs) => some (lhs, rhs) | x => p.iff?

@[inline]

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

Equations

• p.not? = p.app1? `Not

@[inline]

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

Equations

• p.notNot? = match p.not? with | some p => p.not? | none => none

@[inline]

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

Equations

• p.and? = p.app2? `And

@[inline]

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

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

Equations

• p.heq? = p.app4? `HEq

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

Equations

• e.natAdd? = e.app2? `Nat.add

@[inline]

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

Equations

• (Lean.Expr.forallE binderName α β binderInfo).arrow? = if β.hasLooseBVars = true then none else some (α, β)
• x✝.arrow? = none

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

Equations

• e.isEq = e.isAppOfArity `Eq 3

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

Equations

• e.isHEq = e.isAppOfArity `HEq 4

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

Equations

• e.isIte = e.isAppOfArity `ite 5

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

Equations

• e.isDIte = e.isAppOfArity `dite 5

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

Equations

• e.listLit? = Lean.Expr.listLit?.loop✝ e []

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

Equations

• e.arrayLit? = if e.isAppOfArity' `List.toArray 2 = true then e.appArg!'.listLit? else none

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

Recognize α × β

Equations

• e.prod? = e.app2? `Prod

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

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

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Expr.const `Lean.Name.anonymous us).name? = some Lean.Name.anonymous
• (((Lean.Expr.const `Lean.Name.str us).app n).app (Lean.Expr.lit (Lean.Literal.strVal s))).name? = Option.map (fun (x : Lean.Name) => x.str s) n.name?
• (((Lean.Expr.const `Lean.Name.num us).app n).app i).name? = (i.rawNatLit? <|> i.nat?).bind fun (i : Nat) => Option.map (fun (x : Lean.Name) => x.num i) n.name?
• ((Lean.Expr.const `Lean.Name.mkStr1 us).app (Lean.Expr.lit (Lean.Literal.strVal a))).name? = some (Lean.Name.mkStr1 a)
• (((Lean.Expr.const `Lean.Name.mkStr2 us).app (Lean.Expr.lit (Lean.Literal.strVal a1))).app (Lean.Expr.lit (Lean.Literal.strVal a2))).name? = some (Lean.Name.mkStr2 a1 a2)
• x✝.name? = none