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 : Lean.Expr) : Lean.Elab.TermElabM Lean.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.

def Lean.Expr.forallArity : Lean.Expr → Nat

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

Equations

• (Lean.Expr.mdata data b).forallArity = b.forallArity
• (Lean.Expr.forallE binderName binderType body binderInfo).forallArity = 1 + body.forallArity
• x.forallArity = 0

def Lean.Expr.lambdaArity : Lean.Expr → Nat

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

Equations

• (Lean.Expr.mdata data b).lambdaArity = b.lambdaArity
• (Lean.Expr.lam binderName binderType b binderInfo).lambdaArity = 1 + b.lambdaArity
• x.lambdaArity = 0

def Lean.Expr.getAppNumArgs' (e : Lean.Expr) : Nat

Like getAppNumArgs but ignores metadata.

Equations

• e.getAppNumArgs' = Lean.Expr.getAppNumArgs'.go e 0

def Lean.Expr.getAppNumArgs'.go : Lean.Expr → Nat → Nat

Auxiliary definition for getAppNumArgs'.

Equations

• Lean.Expr.getAppNumArgs'.go (Lean.Expr.mdata data b) x = Lean.Expr.getAppNumArgs'.go b x
• Lean.Expr.getAppNumArgs'.go (f.app arg) x = Lean.Expr.getAppNumArgs'.go f (x + 1)
• Lean.Expr.getAppNumArgs'.go x✝ x = x

@[inline]

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

Like withApp but ignores metadata.

Equations

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

@[specialize #[]]

def Lean.Expr.withApp'.go {α : Sort u_1} (k : Lean.Expr → Array Lean.Expr → α) : Lean.Expr → Array Lean.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 : Lean.Expr) : Array Lean.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 : Lean.Expr → m Lean.Expr) (e : Lean.Expr) : m Lean.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 : Lean.Expr) (k : Lean.Expr → Array Lean.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 : Lean.Expr → Array Lean.Expr → α) : Lean.Expr → Array Lean.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 : Lean.Expr) : Array Lean.Expr

Like getAppRevArgs but ignores metadata.

Equations

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

def Lean.Expr.getRevArgD' : Lean.Expr → Nat → Lean.Expr → Lean.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 : Lean.Expr) (i : Nat) (v₀ : Lean.Expr) (n : optParam Nat e.getAppNumArgs') : Lean.Expr

Like getArgD but ignores metadata.

Equations

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

def Lean.Expr.isAppOf' (e : Lean.Expr) (n : Lean.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! : Lean.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!" 115 30 "nat literal expected"

def Lean.Expr.intLit! (e : Lean.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.