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.forallArity (Lean.Expr.mdata data b) = Lean.Expr.forallArity b
• Lean.Expr.forallArity (Lean.Expr.forallE binderName binderType body binderInfo) = 1 + Lean.Expr.forallArity body
• Lean.Expr.forallArity x = 0

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

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

Equations

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

def Lean.Expr.getAppFn' : Lean.Expr → Lean.Expr

Like getAppFn but ignores metadata.

Equations

• Lean.Expr.getAppFn' (Lean.Expr.mdata data b) = Lean.Expr.getAppFn' b
• Lean.Expr.getAppFn' (Lean.Expr.app f arg) = Lean.Expr.getAppFn' f
• Lean.Expr.getAppFn' x = x

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

Like getAppNumArgs but ignores metadata.

Equations

• Lean.Expr.getAppNumArgs' e = 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 (Lean.Expr.app f 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

• Lean.Expr.withApp' e k = let dummy := Lean.mkSort Lean.levelZero; let nargs := Lean.Expr.getAppNumArgs' e; Lean.Expr.withApp'.go k e (mkArray nargs dummy) (nargs - 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 (Lean.Expr.app f a) x✝ x = Lean.Expr.withApp'.go k f (Array.set! x✝ 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

• Lean.Expr.getAppArgs' e = Lean.Expr.withApp' e 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

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

@[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 (Lean.Expr.app f a) x = Lean.Expr.withAppRev'.go k f (Array.push x 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

• Lean.Expr.getAppRevArgs' e = Lean.Expr.withAppRev' e 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.getRevArgD' (Lean.Expr.mdata data b) x✝ x = Lean.Expr.getRevArgD' b x✝ x
• Lean.Expr.getRevArgD' (Lean.Expr.app fn a) 0 x = a
• Lean.Expr.getRevArgD' (Lean.Expr.app f arg) (Nat.succ i) x = Lean.Expr.getRevArgD' f i x
• Lean.Expr.getRevArgD' x✝¹ x✝ x = x

@[inline]

def Lean.Expr.getRevArg!' : Lean.Expr → Nat → Lean.Expr

Like getRevArg! but ignores metadata.

Equations

• Lean.Expr.getRevArg!' (Lean.Expr.mdata data b) x = Lean.Expr.getRevArg!' b x
• Lean.Expr.getRevArg!' (Lean.Expr.app fn a) 0 = a
• Lean.Expr.getRevArg!' (Lean.Expr.app f arg) (Nat.succ i) = Lean.Expr.getRevArg!' f i
• Lean.Expr.getRevArg!' x✝ x = panicWithPosWithDecl "Std.Lean.Expr" "Lean.Expr.getRevArg!'" 113 22 "invalid index"

@[inline]

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

Like getArgD but ignores metadata.

Equations

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

@[inline]

def Lean.Expr.getArg!' (e : Lean.Expr) (i : Nat) (n : optParam Nat (Lean.Expr.getAppNumArgs' e)) : Lean.Expr

Like getArg! but ignores metadata.

Equations

• Lean.Expr.getArg!' e i n = Lean.Expr.getRevArg!' e (n - i - 1)

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

Like isAppOf but ignores metadata.

Equations

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

def Lean.Expr.constName (e : Lean.Expr) : Lean.Name

If the expression is a constant, return that name. Otherwise return Name.anonymous.

Equations

• Lean.Expr.constName e = Option.getD (Lean.Expr.constName? e) Lean.Name.anonymous

def Lean.Expr.getAppFnArgs (e : Lean.Expr) : Lean.Name × Array Lean.Expr

Return the function (name) and arguments of an application.

Equations

• Lean.Expr.getAppFnArgs e = Lean.Expr.withApp e fun (e : Lean.Expr) (a : Array Lean.Expr) => (Lean.Expr.constName e, a)

def Lean.Expr.natLit! : Lean.Expr → Nat

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

Equations

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

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.

def Lean.Expr.nat? (e : Lean.Expr) : Option Nat

Checks if an expression is a "natural number in normal form", i.e. of the form OfNat n, where n matches .lit (.natVal lit) for some lit. and if so returns lit.

Equations

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

def Lean.Expr.int? (e : Lean.Expr) : Option Int

Checks if an expression is an "integer in normal form", i.e. either a natural number in normal form, or the negation of a positive natural number, and if so returns the integer.

Equations

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