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.

@[inline]

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

Like withApp but ignores metadata.

@[inline]

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

Like getAppArgs but ignores metadata.

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

Like traverseApp but ignores metadata.

@[inline]

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

Like withAppRev but ignores metadata.

@[inline]

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

Like getAppRevArgs but ignores metadata.

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

Like getRevArgD but ignores metadata.

@[inline]

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

Like getArgD but ignores metadata.

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

Like isAppOf but ignores metadata.

def Lean.Expr.natLit! : Expr → Nat

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

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.

def Lean.Expr.addLocalVarInfoForBinderIdent (fvar : Expr) (tk : TSyntax `Lean.binderIdent) : MetaM Unit

Annotates a binderIdent with the binder information from an fvar.