Additional operations on Expr and related types

This file defines basic operations on the types expr, name, declaration, level, environment.

This file is mostly for non-tactics.

def Lean.Expr.toSyntax (e : Expr) : Elab.TermElabM Term

Converts an Expr into a Syntax, by creating a fresh metavariable assigned to the expr and returning a named metavariable syntax ?a.

Equations

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

@[reducible, inline, deprecated Lean.Expr.getNumHeadLambdas (since := "2024-10-16")]

abbrev Lean.Expr.lambdaArity : Expr → Nat

Count the number of lambdas at the head of the given expression.

Equations

• Lean.Expr.lambdaArity = Lean.Expr.getNumHeadLambdas

@[reducible, inline, deprecated Lean.Expr.getNumHeadForalls (since := "2024-11-13")]

abbrev Lean.Expr.forallArity : Expr → Nat

Returns the number of leading ∀ binders of an expression. Ignores metadata.

Equations

• Lean.Expr.forallArity = Lean.Expr.getNumHeadForalls

@[inline]

def Lean.Expr.withApp' {α : Sort u_1} (e : Expr) (k : Expr → Array Expr → α) : α

Like withApp but ignores metadata.

Equations

• e.withApp' k = Lean.Expr.withApp'.go k e (Array.replicate e.getAppNumArgs' (Lean.mkSort Lean.levelZero)) (e.getAppNumArgs' - 1)

@[specialize #[]]

def Lean.Expr.withApp'.go {α : Sort u_1} (k : Expr → Array Expr → α) : Expr → Array Expr → Nat → α

Auxiliary definition for withApp'.

Equations

• Lean.Expr.withApp'.go k (Lean.Expr.mdata data b) x✝¹ x✝ = Lean.Expr.withApp'.go k b x✝¹ x✝
• Lean.Expr.withApp'.go k (f.app a) x✝¹ x✝ = Lean.Expr.withApp'.go k f (x✝¹.set! x✝ a) (x✝ - 1)
• Lean.Expr.withApp'.go k x✝² x✝¹ x✝ = k x✝² x✝¹

@[inline]

def Lean.Expr.getAppArgs' (e : Expr) : Array Expr

Like getAppArgs but ignores metadata.

Equations

• e.getAppArgs' = e.withApp' fun (x : Lean.Expr) (as : Array Lean.Expr) => as

def Lean.Expr.traverseApp' {m : Type → Type u_1} [Monad m] (f : Expr → m Expr) (e : Expr) : m Expr

Like traverseApp but ignores metadata.

Equations

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

@[inline]

def Lean.Expr.withAppRev' {α : Sort u_1} (e : Expr) (k : Expr → Array Expr → α) : α

Like withAppRev but ignores metadata.

Equations

• e.withAppRev' k = Lean.Expr.withAppRev'.go k e (Array.mkEmpty e.getAppNumArgs')

@[specialize #[]]

def Lean.Expr.withAppRev'.go {α : Sort u_1} (k : Expr → Array Expr → α) : Expr → Array Expr → α

Auxiliary definition for withAppRev'.

Equations

• Lean.Expr.withAppRev'.go k (Lean.Expr.mdata data b) x✝ = Lean.Expr.withAppRev'.go k b x✝
• Lean.Expr.withAppRev'.go k (f.app a) x✝ = Lean.Expr.withAppRev'.go k f (x✝.push a)
• Lean.Expr.withAppRev'.go k x✝¹ x✝ = k x✝¹ x✝

@[inline]

def Lean.Expr.getAppRevArgs' (e : Expr) : Array Expr

Like getAppRevArgs but ignores metadata.

Equations

• e.getAppRevArgs' = e.withAppRev' fun (x : Lean.Expr) (as : Array Lean.Expr) => as

def Lean.Expr.getRevArgD' : Expr → Nat → Expr → Expr

Like getRevArgD but ignores metadata.

Equations

• (Lean.Expr.mdata data b).getRevArgD' x✝¹ x✝ = b.getRevArgD' x✝¹ x✝
• (fn.app a).getRevArgD' 0 x✝ = a
• (f.app arg).getRevArgD' i.succ x✝ = f.getRevArgD' i x✝
• x✝².getRevArgD' x✝¹ x✝ = x✝

@[inline]

def Lean.Expr.getArgD' (e : Expr) (i : Nat) (v₀ : Expr) (n : Nat := e.getAppNumArgs') : Expr

Like getArgD but ignores metadata.

Equations

• e.getArgD' i v₀ n = e.getRevArgD' (n - i - 1) v₀

def Lean.Expr.isAppOf' (e : Expr) (n : Name) : Bool

Like isAppOf but ignores metadata.

Equations

• e.isAppOf' n = match e.getAppFn' with | Lean.Expr.const c us => c == n | x => false

def Lean.Expr.natLit! : Expr → Nat

Turns an expression that is a natural number literal into a natural number.

Equations

• (Lean.Expr.lit (Lean.Literal.natVal v)).natLit! = v
• x✝.natLit! = panicWithPosWithDecl "Batteries.Lean.Expr" "Lean.Expr.natLit!" 95 30 "nat literal expected"

def Lean.Expr.intLit! (e : Expr) : Int

Turns an expression that is a constructor of Int applied to a natural number literal into an integer.

Equations

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