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.

ink

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.

ink

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

ink

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

ink

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

ink

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

Like getAppNumArgs but ignores metadata.

Equations

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

ink

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

ink

@[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)

ink

@[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

ink

@[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 as => as

ink

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

Like traverseApp but ignores metadata.

Equations

• Lean.Expr.traverseApp' f e = Lean.Expr.withApp' e fun fn args => do let __do_lift ← f fn let __do_lift_1 ← Array.mapM f args pure (Lean.mkAppN __do_lift __do_lift_1)

ink

@[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))

ink

@[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

ink

@[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 as => as

ink

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

ink

@[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"

ink

@[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₀

ink

@[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)

ink

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