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.
Instances For
Returns the number of leading ∀
binders of an expression. Ignores metadata.
Equations
- (Lean.Expr.mdata data b).forallArity = b.forallArity
- (Lean.Expr.forallE binderName binderType body binderInfo).forallArity = 1 + body.forallArity
- x.forallArity = 0
Instances For
Returns the number of leading λ
binders of an expression. Ignores metadata.
Equations
- (Lean.Expr.mdata data b).lambdaArity = b.lambdaArity
- (Lean.Expr.lam binderName binderType b binderInfo).lambdaArity = 1 + b.lambdaArity
- x.lambdaArity = 0
Instances For
Like getAppNumArgs
but ignores metadata.
Equations
- e.getAppNumArgs' = Lean.Expr.getAppNumArgs'.go e 0
Instances For
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 (f.app arg) x = Lean.Expr.getAppNumArgs'.go f (x + 1)
- Lean.Expr.getAppNumArgs'.go x✝ x = x
Instances For
Like withApp
but ignores metadata.
Equations
- e.withApp' k = let dummy := Lean.mkSort Lean.levelZero; let nargs := e.getAppNumArgs'; Lean.Expr.withApp'.go k e (mkArray nargs dummy) (nargs - 1)
Instances For
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✝
Instances For
Like withAppRev
but ignores metadata.
Equations
- e.withAppRev' k = Lean.Expr.withAppRev'.go k e (Array.mkEmpty e.getAppNumArgs')
Instances For
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
Instances For
Like isAppOf
but ignores metadata.
Equations
- e.isAppOf' n = match e.getAppFn' with | Lean.Expr.const c us => c == n | x => false
Instances For
Turns an expression that is a natural number literal into a natural number.
Equations
- x.natLit! = match x with | Lean.Expr.lit (Lean.Literal.natVal v) => v | x => panicWithPosWithDecl "Batteries.Lean.Expr" "Lean.Expr.natLit!" 115 30 "nat literal expected"
Instances For
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.