Documentation

Std.Lean.Expr

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.

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.

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

Equations

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

Equations

Like getAppNumArgs but ignores metadata.

Equations
@[inline]
def Lean.Expr.withApp' {α : Sort u_1} (e : Lean.Expr) (k : Lean.ExprArray Lean.Exprα) :
α

Like withApp but ignores metadata.

Equations
@[specialize #[]]
def Lean.Expr.withApp'.go {α : Sort u_1} (k : Lean.ExprArray Lean.Exprα) :
Lean.ExprArray Lean.ExprNatα

Auxiliary definition for withApp'.

Equations
@[inline]

Like getAppArgs but ignores metadata.

Equations
def Lean.Expr.traverseApp' {m : TypeType u_1} [inst : Monad m] (f : Lean.Exprm Lean.Expr) (e : Lean.Expr) :

Like traverseApp but ignores metadata.

Equations
@[inline]
def Lean.Expr.withAppRev' {α : Sort u_1} (e : Lean.Expr) (k : Lean.ExprArray Lean.Exprα) :
α

Like withAppRev but ignores metadata.

Equations
@[inline]

Like getAppRevArgs but ignores metadata.

Equations
@[inline]

Like getRevArg! but ignores metadata.

Equations
@[inline]

Like getArgD but ignores metadata.

Equations
@[inline]

Like getArg! but ignores metadata.

Equations

Like isAppOf but ignores metadata.

Equations