Documentation

Batteries.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.
@[reducible, inline, deprecated Lean.Expr.getNumHeadLambdas]

Count the number of lambdas at the head of the given expression.

Equations
@[reducible, inline, deprecated Lean.Expr.getNumHeadForalls]

Returns the number of leading binders of an expression. 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} [Monad m] (f : Lean.Exprm Lean.Expr) (e : 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.ExprArray Lean.Exprα) :
α

Like withAppRev but ignores metadata.

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

Auxiliary definition for withAppRev'.

Equations
@[inline]

Like getAppRevArgs but ignores metadata.

Equations

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 : Nat := e.getAppNumArgs') :

Like getArgD but ignores metadata.

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

Like isAppOf but ignores metadata.

Equations

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

Equations

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.