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.
Count the number of lambdas at the head of the given expression.
Returns the number of leading ∀
binders of an expression. Ignores metadata.
Like withApp
but ignores metadata.
Equations
- e.withApp' k = Lean.Expr.withApp'.go k e (mkArray e.getAppNumArgs' (Lean.mkSort Lean.levelZero)) (e.getAppNumArgs' - 1)
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 (f.app a) x✝ x = Lean.Expr.withApp'.go k f (x✝.set! x a) (x - 1)
- Lean.Expr.withApp'.go k x✝¹ x✝ x = k x✝¹ x✝
Like withAppRev
but ignores metadata.
Equations
- e.withAppRev' k = Lean.Expr.withAppRev'.go k e (Array.mkEmpty e.getAppNumArgs')
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 (f.app a) x = Lean.Expr.withAppRev'.go k f (x.push a)
- Lean.Expr.withAppRev'.go k x✝ x = k x✝ x
Like isAppOf
but ignores metadata.
Equations
- e.isAppOf' n = match e.getAppFn' with | Lean.Expr.const c us => c == n | x => false
Turns an expression that is a natural number literal into a natural number.
Equations
- (Lean.Expr.lit (Lean.Literal.natVal v)).natLit! = v
- x.natLit! = panicWithPosWithDecl "Batteries.Lean.Expr" "Lean.Expr.natLit!" 95 30 "nat literal expected"
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.