Mathlib.Lean.Expr.Basic

Lean.BinderInfo.brackets definition

: BinderInfo → String × String

Full source

/-- The brackets corresponding to a given `BinderInfo`. -/
def brackets : BinderInfo → StringString × String
  | BinderInfo.implicit => ("{", "}")
  | BinderInfo.strictImplicit => ("{{", "}}")
  | BinderInfo.instImplicit => ("[", "]")
  | _ => ("(", ")")

Brackets for binder types

Informal description

The function takes a `BinderInfo` value and returns a pair of strings representing the opening and closing brackets corresponding to the binder type: - Implicit binders use curly braces `{` and `}` - Strict implicit binders use double curly braces `{{` and `}}` - Instance implicit binders use square brackets `[` and `]` - All other binders use parentheses `(` and `)`

Lean.Name.mapPrefix definition

(f : Name → Option Name) (n : Name) : Name

Full source

/-- Find the largest prefix `n` of a `Name` such that `f n != none`, then replace this prefix
with the value of `f n`. -/
def mapPrefix (f : Name → Option Name) (n : Name) : Name := Id.run do
  if let some n' := f n then return n'
  match n with
  | anonymous => anonymous
  | str n' s => mkStr (mapPrefix f n') s
  | num n' i => mkNum (mapPrefix f n') i

Name prefix mapping

Informal description

Given a function `f` from names to optional names and a name `n`, this function finds the largest prefix `n'` of `n` such that `f n'` returns some value, then replaces this prefix with the value of `f n'`. If no such prefix exists, it recursively applies the same operation to the components of `n`.

Lean.Name.fromComponents definition

: List Name → Name

Full source

/-- Build a name from components.
For example, ``from_components [`foo, `bar]`` becomes ``` `foo.bar```.
It is the inverse of `Name.components` on list of names that have single components. -/
def fromComponents : List Name → Name := go .anonymous where
  /-- Auxiliary for `Name.fromComponents` -/
  go : Name → List Name → Name
  | n, []        => n
  | n, s :: rest => go (s.updatePrefix n) rest

Name construction from components

Informal description

The function constructs a name by combining a list of name components with periods. For example, given the list ``[`foo, `bar]``, it produces the name `` `foo.bar``. This operation is the inverse of `Name.components` when applied to lists of names that each consist of a single component.

Lean.Name.updateLast definition

(f : String → String) : Name → Name

Full source

/-- Update the last component of a name. -/
def updateLast (f : String → String) : Name → Name
  | .str n s => .str n (f s)
  | n        => n

Update last component of a name

Informal description

The function `Lean.Name.updateLast` takes a string transformation function `f` and a name `n`, and returns a new name where the last component of `n` (if it is a string) is replaced by applying `f` to it. If `n` does not have a string component, it remains unchanged.

Lean.Name.lastComponentAsString definition

: Name → String

Full source

/-- Get the last field of a name as a string.
Doesn't raise an error when the last component is a numeric field. -/
def lastComponentAsString : Name → String
  | .str _ s => s
  | .num _ n => toString n
  | .anonymous => ""

Last component of a name as string

Informal description

The function extracts the last component of a name as a string. For a string component, it returns the string itself; for a numeric component, it converts the number to a string; and for an anonymous name, it returns an empty string.

Lean.Name.splitAt definition

(nm : Name) (n : Nat) : Name × Name

Full source

/-- `nm.splitAt n` splits a name `nm` in two parts, such that the *second* part has depth `n`,
i.e. `(nm.splitAt n).2.getNumParts = n` (assuming `nm.getNumParts ≥ n`).
Example: ``splitAt `foo.bar.baz.back.bat 1 = (`foo.bar.baz.back, `bat)``. -/
def splitAt (nm : Name) (n : Nat) : NameName × Name :=
  let (nm2, nm1) := nm.componentsRev.splitAt n
  (.fromComponents <| nm1.reverse, .fromComponents <| nm2.reverse)

Name splitting at specified depth

Informal description

Given a name `nm` and a natural number `n`, the function `splitAt` splits `nm` into two parts such that the second part has depth `n`. That is, if `nm` has at least `n` components, then the second part of the result will consist of the last `n` components of `nm`, and the first part will consist of the remaining components. For example, splitting the name `` `foo.bar.baz.back.bat`` at depth `1` results in ``(`foo.bar.baz.back, `bat)``.

Lean.Name.isPrefixOf? definition

(pre nm : Name) : Option Name

Full source

/-- `isPrefixOf? pre nm` returns `some post` if `nm = pre ++ post`.
Note that this includes the case where `nm` has multiple more namespaces.
If `pre` is not a prefix of `nm`, it returns `none`. -/
def isPrefixOf? (pre nm : Name) : Option Name :=
  if pre == nm then
    some anonymous
  else match nm with
  | anonymous => none
  | num p' a => (isPrefixOf? pre p').map (·.num a)
  | str p' s => (isPrefixOf? pre p').map (·.str s)

Name prefix check with remainder extraction

Informal description

Given two names `pre` and `nm`, the function checks if `pre` is a prefix of `nm`. If it is, it returns the remaining part of `nm` after the prefix `pre` (which could be multiple namespaces deep). If `pre` is not a prefix of `nm`, it returns `none`. Specifically: - If `pre` exactly matches `nm`, it returns `some anonymous`. - For compound names (numeric or string-based), it recursively checks the prefix and constructs the result accordingly.

Lean.Name.isBlackListed definition

{m} [Monad m] [MonadEnv m] (declName : Name) : m Bool

Full source

def isBlackListed {m} [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
  if declName == ``sorryAx then return true
  if declName matches .str _ "inj" then return true
  if declName matches .str _ "noConfusionType" then return true
  let env ← getEnv
  pure <| declName.isInternalDetail
   || isAuxRecursor env declName
   || isNoConfusion env declName
  <||> isRec declName <||> isMatcher declName

Blacklisted declaration name check

Informal description

Given a monadic environment `m` and a declaration name `declName`, the function checks whether `declName` is blacklisted. A name is blacklisted if it is one of the following: 1. The special name ``sorryAx`` 2. A name ending with the suffix "inj" 3. A name ending with the suffix "noConfusionType" 4. An internal detail name 5. An auxiliary recursor 6. A no-confusion theorem 7. A recursive declaration 8. A matcher function

Lean.ConstantInfo.isDef definition

: ConstantInfo → Bool

Full source

/-- Checks whether this `ConstantInfo` is a definition. -/
def isDef : ConstantInfo → Bool
  | defnInfo _ => true
  | _          => false

Check if ConstantInfo is a definition

Informal description

The function checks whether a given `ConstantInfo` object represents a definition. It returns `true` if the object is a definition and `false` otherwise.

Lean.ConstantInfo.isThm definition

: ConstantInfo → Bool

Full source

/-- Checks whether this `ConstantInfo` is a theorem. -/
def isThm : ConstantInfo → Bool
  | thmInfo _ => true
  | _          => false

Check if ConstantInfo is a theorem

Informal description

The function checks whether a given `ConstantInfo` object represents a theorem, returning `true` if it does and `false` otherwise.

Lean.ConstantInfo.updateConstantVal definition

: ConstantInfo → ConstantVal → ConstantInfo

Full source

/-- Update `ConstantVal` (the data common to all constructors of `ConstantInfo`)
in a `ConstantInfo`. -/
def updateConstantVal : ConstantInfo → ConstantVal → ConstantInfo
  | defnInfo   info, v => defnInfo   {info with toConstantVal := v}
  | axiomInfo  info, v => axiomInfo  {info with toConstantVal := v}
  | thmInfo    info, v => thmInfo    {info with toConstantVal := v}
  | opaqueInfo info, v => opaqueInfo {info with toConstantVal := v}
  | quotInfo   info, v => quotInfo   {info with toConstantVal := v}
  | inductInfo info, v => inductInfo {info with toConstantVal := v}
  | ctorInfo   info, v => ctorInfo   {info with toConstantVal := v}
  | recInfo    info, v => recInfo    {info with toConstantVal := v}

Update shared constant data in `ConstantInfo`

Informal description

The function updates the `ConstantVal` field (common data shared by all constructors of `ConstantInfo`) in a `ConstantInfo` structure, preserving the constructor type (e.g., `defnInfo`, `axiomInfo`, etc.) while replacing the shared `ConstantVal` data with the provided value.

Lean.ConstantInfo.updateName definition

(c : ConstantInfo) (name : Name) : ConstantInfo

Full source

/-- Update the name of a `ConstantInfo`. -/
def updateName (c : ConstantInfo) (name : Name) : ConstantInfo :=
  c.updateConstantVal {c.toConstantVal with name}

Update name in `ConstantInfo`

Informal description

The function updates the name field of a `ConstantInfo` structure while preserving all other fields. Given a `ConstantInfo` object `c` and a new name, it returns a new `ConstantInfo` object with the same constructor type and all other fields unchanged, except for the name which is updated to the provided value.

Lean.ConstantInfo.updateType definition

(c : ConstantInfo) (type : Expr) : ConstantInfo

Full source

/-- Update the type of a `ConstantInfo`. -/
def updateType (c : ConstantInfo) (type : Expr) : ConstantInfo :=
  c.updateConstantVal {c.toConstantVal with type}

Update type of a constant declaration

Informal description

The function updates the type field of a `ConstantInfo` structure, preserving all other fields while replacing the type with the provided expression.

Lean.ConstantInfo.updateLevelParams definition

(c : ConstantInfo) (levelParams : List Name) : ConstantInfo

Full source

/-- Update the level parameters of a `ConstantInfo`. -/
def updateLevelParams (c : ConstantInfo) (levelParams : List Name) :
    ConstantInfo :=
  c.updateConstantVal {c.toConstantVal with levelParams}

Update level parameters in `ConstantInfo`

Informal description

The function updates the level parameters of a `ConstantInfo` structure `c` to the given list of names `levelParams`, while preserving all other fields of the structure.

Lean.ConstantInfo.updateValue definition

: ConstantInfo → Expr → ConstantInfo

Full source

/-- Update the value of a `ConstantInfo`, if it has one. -/
def updateValue : ConstantInfo → Expr → ConstantInfo
  | defnInfo   info, v => defnInfo   {info with value := v}
  | thmInfo    info, v => thmInfo    {info with value := v}
  | opaqueInfo info, v => opaqueInfo {info with value := v}
  | d, _ => d

Update value of a constant declaration

Informal description

Given a `ConstantInfo` structure `c` and an expression `v`, this function updates the `value` field of `c` to `v` if `c` is a definition, theorem, or opaque declaration. For other types of `ConstantInfo`, the function returns the original structure unchanged.

Lean.ConstantInfo.toDeclaration! definition

: ConstantInfo → Declaration

Full source

/-- Turn a `ConstantInfo` into a declaration. -/
def toDeclaration! : ConstantInfo → Declaration
  | defnInfo   info => Declaration.defnDecl info
  | thmInfo    info => Declaration.thmDecl     info
  | axiomInfo  info => Declaration.axiomDecl   info
  | opaqueInfo info => Declaration.opaqueDecl  info
  | quotInfo   _ => panic! "toDeclaration for quotInfo not implemented"
  | inductInfo _ => panic! "toDeclaration for inductInfo not implemented"
  | ctorInfo   _ => panic! "toDeclaration for ctorInfo not implemented"
  | recInfo    _ => panic! "toDeclaration for recInfo not implemented"

Conversion from ConstantInfo to Declaration

Informal description

The function converts a `ConstantInfo` object into a `Declaration` object. The conversion depends on the type of `ConstantInfo`: - For definition info (`defnInfo`), it creates a definition declaration. - For theorem info (`thmInfo`), it creates a theorem declaration. - For axiom info (`axiomInfo`), it creates an axiom declaration. - For opaque info (`opaqueInfo`), it creates an opaque declaration. - For quotient info (`quotInfo`), induction info (`inductInfo`), constructor info (`ctorInfo`), and recursion info (`recInfo`), the function panics with an error message indicating that the conversion is not implemented.

Lean.mkConst' definition

(constName : Name) : MetaM Expr

Full source

/-- Same as `mkConst`, but with fresh level metavariables. -/
def mkConst' (constName : Name) : MetaM Expr := do
  return mkConst constName (← (← getConstInfo constName).levelParams.mapM fun _ => mkFreshLevelMVar)

Create constant expression with fresh level metavariables

Informal description

The function creates a constant expression with the given name `constName`, where each level parameter of the constant is replaced with a fresh metavariable. This is similar to `mkConst` but with fresh level metavariables instead of explicit levels.

Lean.Expr.bvarIdx? definition

: Expr → Option Nat

Full source

def bvarIdx? : Expr → Option Nat
  | bvar idx => some idx
  | _        => none

Bound variable index extractor

Informal description

The function takes an expression `e` and returns the index of `e` if it is a bound variable (denoted by `bvar`), and returns `none` otherwise.

Lean.Expr.getAppApps definition

(e : Expr) : Array Expr

Full source

/-- Given `f a b c`, return `#[f a, f a b, f a b c]`.
Each entry in the array is an `Expr.app`,
and this array has the same length as the one returned by `Lean.Expr.getAppArgs`. -/
@[inline]
def getAppApps (e : Expr) : Array Expr :=
  let dummy := mkSort levelZero
  let nargs := e.getAppNumArgs
  getAppAppsAux e (.replicate nargs dummy) (nargs-1)

Successive applications of a function expression

Informal description

Given an expression `e` of the form `f a₁ a₂ ... aₙ`, this function returns an array of expressions `#[f a₁, f a₁ a₂, ..., f a₁ a₂ ... aₙ]`, where each entry is obtained by successively applying the arguments to the function `f`. The length of the resulting array matches the number of arguments in the original expression.

Lean.Expr.eraseProofs definition

(e : Expr) : MetaM Expr

Full source

/-- Erase proofs in an expression by replacing them with `sorry`s.

This function replaces all proofs in the expression
and in the types that appear in the expression
by `sorryAx`s.
The resulting expression has the same type as the old one.

It is useful, e.g., to verify if the proof-irrelevant part of a definition depends on a variable.
-/
def eraseProofs (e : Expr) : MetaM Expr :=
  Meta.transform (skipConstInApp := true) e
    (pre := fun e => do
      if (← Meta.isProof e) then
        return .continue (← mkSorry (← inferType e) true)
      else
        return .continue)

Proof erasure in Lean expressions

Informal description

The function `eraseProofs` takes a Lean expression `e` and replaces all proof subexpressions within `e` and its types with `sorry` placeholders. The resulting expression maintains the same type as the original. This is useful for checking whether the proof-irrelevant parts of a definition depend on certain variables.

Lean.Expr.type? definition

: Expr → Option Level

Full source

/-- If an `Expr` has the form `Type u`, then return `some u`, otherwise `none`. -/
def type? : Expr → Option Level
  | .sort u => u.dec
  | _ => none

Extract level from type universe expression

Informal description

Given an expression `e`, if `e` is of the form `Type u` (i.e., a sort), then return the level `u`; otherwise return `none`. This function checks whether an expression represents a type universe and extracts its level if it does.

Lean.Expr.isConstantApplication definition

(e : Expr)

Full source

/-- `isConstantApplication e` checks whether `e` is syntactically an application of the form
`(fun x₁ ⋯ xₙ => H) y₁ ⋯ yₙ` where `H` does not contain the variable `xₙ`. In other words,
it does a syntactic check that the expression does not depend on `yₙ`. -/
def isConstantApplication (e : Expr) :=
  e.isApp && aux e.getAppNumArgs'.pred e.getAppFn' e.getAppNumArgs'
where
  /-- `aux depth e n` checks whether the body of the `n`-th lambda of `e` has loose bvar
    `depth - 1`. -/
  aux (depth : Nat) : Expr → Nat → Bool
    | .lam _ _ b _, n + 1  => aux depth b n
    | e, 0  => !e.hasLooseBVar (depth - 1)
    | _, _ => false

Syntactic check for constant application

Informal description

The function `isConstantApplication` checks whether an expression `e` is syntactically of the form `(fun x₁ ⋯ xₙ => H) y₁ ⋯ yₙ` where `H` does not contain the variable `xₙ`. In other words, it verifies that the expression does not syntactically depend on the last argument `yₙ`.

Lean.Expr.letDepth definition

: Expr → Nat

Full source

/-- Counts the immediate depth of a nested `let` expression. -/
def letDepth : Expr → Nat
  | .letE _ _ _ b _ => b.letDepth + 1
  | _ => 0

Depth of nested let expressions

Informal description

The function `letDepth` computes the immediate nesting depth of `let` expressions in a given expression. For a `let` expression, it recursively counts the depth of the body and adds 1. For all other expressions, it returns 0.

Lean.Expr.ensureHasNoMVars definition

(e : Expr) : MetaM Unit

Full source

/-- Check that an expression contains no metavariables (after instantiation). -/
-- There is a `TacticM` level version of this, but it's useful to have in `MetaM`.
def ensureHasNoMVars (e : Expr) : MetaM Unit := do
  let e ← instantiateMVars e
  if e.hasExprMVar then
    throwError "tactic failed, resulting expression contains metavariables{indentExpr e}"

Check for absence of metavariables in expression

Informal description

The function checks whether a given expression `e` contains no metavariables after instantiation. If metavariables are found, it throws an error indicating that the expression contains metavariables.

Lean.Expr.ofNat definition

(α : Expr) (n : Nat) : MetaM Expr

Full source

/-- Construct the term of type `α` for a given natural number
(doing typeclass search for the `OfNat` instance required). -/
def ofNat (α : Expr) (n : Nat) : MetaM Expr := do
  mkAppOptM ``OfNat.ofNat #[α, mkRawNatLit n, none]

Construction of natural number term via OfNat instance

Informal description

The function constructs a term of type `α` for a given natural number `n` by searching for and applying the appropriate `OfNat` instance.

Lean.Expr.ofInt definition

(α : Expr) : Int → MetaM Expr

Full source

/-- Construct the term of type `α` for a given integer
(doing typeclass search for the `OfNat` and `Neg` instances required). -/
def ofInt (α : Expr) : Int → MetaM Expr
  | Int.ofNat n => Expr.ofNat α n
  | Int.negSucc n => do mkAppM ``Neg.neg #[← Expr.ofNat α (n+1)]

Construction of integer term via OfNat and Neg instances

Informal description

The function constructs a term of type `α` for a given integer `n` by either: - Using the `OfNat` instance when `n` is non-negative, or - Applying the `Neg.neg` function to the term constructed from `n+1` when `n` is negative.

Lean.Expr.numeral? definition

(e : Expr) : Option Nat

Full source

/--
Return `some n` if `e` is one of the following
- a nat literal (numeral)
- `Nat.zero`
- `Nat.succ x` where `isNumeral x`
- `OfNat.ofNat _ x _` where `isNumeral x` -/
partial def numeral? (e : Expr) : Option Nat :=
  if let somesome n := e.rawNatLit? then n
  else
    let e := e.consumeMData -- `OfNat` numerals may have `no_index` around them from `ofNat()`
    let f := e.getAppFn
    if !f.isConst then none
    else
      let fName := f.constName!
      if fName == ``Nat.succ && e.getAppNumArgs == 1 then (numeral? e.appArg!).map Nat.succ
      else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then numeral? (e.getArg! 1)
      else if fName == ``Nat.zero && e.getAppNumArgs == 0 then some 0
      else none

Check if expression is a natural number numeral

Informal description

The function checks if the given expression `e` represents a natural number numeral and returns `some n` if it does. The expression `e` is considered a numeral if it is: - A natural number literal, - The constant `Nat.zero`, - An application of `Nat.succ` to a numeral, or - An application of `OfNat.ofNat` where the second argument is a numeral.

Lean.Expr.zero? definition

(e : Expr) : Bool

Full source

/-- Test if an expression is either `Nat.zero`, or `OfNat.ofNat 0`. -/
def zero? (e : Expr) : Bool :=
  match e.numeral? with
  | somesome 0 => true
  | _ => false

Check if expression is zero

Informal description

The function checks if the given expression `e` represents the natural number zero, either as `Nat.zero` or as `OfNat.ofNat 0`. It returns `true` if `e` is zero and `false` otherwise.

Lean.Expr.ne?' definition

(e : Expr) : Option (Expr × Expr × Expr)

Full source

/-- Tests is if an expression matches either `x ≠ y` or `¬ (x = y)`.
If it matches, returns `some (type, x, y)`. -/
def ne?' (e : Expr) : Option (ExprExpr × Expr × Expr) :=
  e.ne? <|> (e.not? >>= Expr.eq?)

Check for inequality expressions

Informal description

Given an expression `e`, this function checks if `e` matches either the form `x ≠ y` or `¬ (x = y)`. If it does, it returns `some (type, x, y)`, where `type` is the type of `x` and `y`, and `x` and `y` are the expressions being compared. Otherwise, it returns `none`.

Lean.Expr.le? definition

(p : Expr) : Option (Expr × Expr × Expr)

Full source

/-- `Lean.Expr.le? e` takes `e : Expr` as input.
If `e` represents `a ≤ b`, then it returns `some (t, a, b)`, where `t` is the Type of `a`,
otherwise, it returns `none`. -/
@[inline] def le? (p : Expr) : Option (ExprExpr × Expr × Expr) := do
  let (type, _, lhs, rhs) ← p.app4? ``LE.le
  return (type, lhs, rhs)

Extract components of a ≤ expression

Informal description

The function takes an expression `p` and checks if it represents an inequality of the form `a ≤ b`. If so, it returns the type of `a` along with the expressions for `a` and `b`; otherwise, it returns `none`.

Lean.Expr.lt? definition

(p : Expr) : Option (Expr × Expr × Expr)

Full source

/-- `Lean.Expr.lt? e` takes `e : Expr` as input.
If `e` represents `a < b`, then it returns `some (t, a, b)`, where `t` is the Type of `a`,
otherwise, it returns `none`. -/
@[inline] def lt? (p : Expr) : Option (ExprExpr × Expr × Expr) := do
  let (type, _, lhs, rhs) ← p.app4? ``LT.lt
  return (type, lhs, rhs)

Expression strict inequality decomposition

Informal description

The function `Lean.Expr.lt?` takes an expression `e` as input. If `e` represents a strict inequality `a < b`, then it returns the type `t` of `a` along with the expressions `a` and `b`; otherwise, it returns `none`.

Lean.Expr.sides? definition

(ty : Expr) : Option (Expr × Expr × Expr × Expr)

Full source

/-- Given a proposition `ty` that is an `Eq`, `Iff`, or `HEq`, returns `(tyLhs, lhs, tyRhs, rhs)`,
where `lhs : tyLhs` and `rhs : tyRhs`,
and where `lhs` is related to `rhs` by the respective relation.

See also `Lean.Expr.iff?`, `Lean.Expr.eq?`, and `Lean.Expr.heq?`. -/
def sides? (ty : Expr) : Option (ExprExpr × Expr × Expr × Expr) :=
  if let some (lhs, rhs) := ty.iff? then
    some (.sort .zero, lhs, .sort .zero, rhs)
  else if let some (ty, lhs, rhs) := ty.eq? then
    some (ty, lhs, ty, rhs)
  else
    ty.heq?

Decomposition of equality-like propositions into left and right sides

Informal description

Given a proposition `ty` that represents an equality (`Eq`), equivalence (`Iff`), or heterogeneous equality (`HEq`), this function returns a tuple `(tyLhs, lhs, tyRhs, rhs)`, where `lhs` is of type `tyLhs`, `rhs` is of type `tyRhs`, and `lhs` is related to `rhs` by the respective relation (equality, equivalence, or heterogeneous equality).

Lean.Expr.modifyAppArgM definition

{M : Type → Type u} [Functor M] [Pure M] (modifier : Expr → M Expr) : Expr → M Expr

Full source

def modifyAppArgM {M : Type → Type u} [Functor M] [Pure M]
    (modifier : Expr → M Expr) : Expr → M Expr
  | app f a => mkApp f <$> modifier a
  | e => pure e

Monadic modification of application argument

Informal description

Given a monadic function `modifier` that transforms expressions, this function applies `modifier` to the argument of an application expression `f a`, returning a new application expression with the modified argument. For non-application expressions, it returns the expression unchanged in the monadic context.

Lean.Expr.modifyRevArg definition

(modifier : Expr → Expr) : Nat → Expr → Expr

Full source

def modifyRevArg (modifier : Expr → Expr) : Nat → Expr → Expr
  | 0,     (.app f x) => .app f (modifier x)
  | (i+1), (.app f x) => .app (modifyRevArg modifier i f) x
  | _, e => e

Modify the `i`-th argument from the right in an expression

Informal description

The function `modifyRevArg` takes a modifier function `modifier : Expr → Expr`, a natural number `i`, and an expression `e`, and returns a new expression where the `i`-th argument (counting from the right) of `e` is modified by applying `modifier` to it. If `e` is not an application or `i` is out of bounds, the function returns `e` unchanged. More precisely: - If `e` is an application `.app f x` and `i = 0`, the function returns `.app f (modifier x)`. - If `e` is an application `.app f x` and `i = k+1`, the function recursively modifies the `k`-th argument of `f` from the right. - In all other cases, the function returns `e` unchanged.

Lean.Expr.getRevArg? definition

: Expr → Nat → Option Expr

Full source

def getRevArg? : Expr → Nat → Option Expr
  | app _ a, 0   => a
  | app f _, i+1 => getRevArg! f i
  | _,       _   => none

Reverse argument accessor for expressions

Informal description

The function retrieves the `i`-th argument from the end of an application expression `e`. If `e` is an application `f a` and `i = 0`, it returns `a`. If `e` is an application `f a` and `i > 0`, it recursively looks for the `(i-1)`-th argument in `f`. If `e` is not an application or the index is out of bounds, it returns `none`.

Lean.Expr.renameBVar definition

(e : Expr) (old new : Name) : Expr

Full source

/-- Traverses an expression `e` and renames bound variables named `old` to `new`. -/
def renameBVar (e : Expr) (old new : Name) : Expr :=
  match e with
  | app fn arg => app (fn.renameBVar old new) (arg.renameBVar old new)
  | lam n ty bd bi =>
    lam (if n == old then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi
  | forallE n ty bd bi =>
    forallE (if n == old then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi
  | mdata d e' => mdata d (e'.renameBVar old new)
  | e => e

Bound variable renaming in expressions

Informal description

The function takes an expression `e` and renames all bound variables named `old` to `new` in `e`. It traverses the expression structure, handling applications, lambda abstractions, universal quantifiers, and metadata expressions, while leaving other types of expressions unchanged.

Lean.Expr.getBinderName definition

(e : Expr) : MetaM (Option Name)

Full source

/-- `getBinderName e` returns `some n` if `e` is an expression of the form `∀ n, ...`
and `none` otherwise. -/
def getBinderName (e : Expr) : MetaM (Option Name) := do
  match ← withReducible (whnf e) with
  | .forallE (binderName := n) .. | .lam (binderName := n) .. => pure (some n)
  | _ => pure none

Get bound variable name from expression

Informal description

The function `getBinderName` takes an expression `e` and returns `some n` if `e` is a universal quantifier (`∀ n, ...`) or a lambda abstraction (`λ n, ...`), where `n` is the bound variable name. Otherwise, it returns `none`.

Lean.Expr.addLocalVarInfoForBinderIdent definition

(fvar : Expr) (tk : TSyntax `` binderIdent) : MetaM Unit

Full source

/-- Annotates a `binderIdent` with the binder information from an `fvar`. -/
def addLocalVarInfoForBinderIdent (fvar : Expr) (tk : TSyntax ``binderIdent) : MetaM Unit :=
  -- the only TermElabM thing we do in `addLocalVarInfo` is check inPattern,
  -- which we assume is always false for this function
  discard <| TermElabM.run do
    match tk with
    | `(binderIdent| $n:ident) => Elab.Term.addLocalVarInfo n fvar
    | tk => Elab.Term.addLocalVarInfo (Unhygienic.run `(_%$tk)) fvar

Annotate binder identifier with free variable information

Informal description

Given a free variable expression `fvar` and a syntax tree node `tk` representing a binder identifier, this function annotates the binder identifier with the binder information from the free variable. If `tk` is an identifier, it directly adds local variable information; otherwise, it processes the syntax tree node in an unhygienic manner to add the information.

Lean.Expr.mkDirectProjection definition

(e : Expr) (fieldName : Name) : MetaM Expr

Full source

/-- If `e` has a structure as type with field `fieldName`, `mkDirectProjection e fieldName` creates
the projection expression `e.fieldName` -/
def mkDirectProjection (e : Expr) (fieldName : Name) : MetaM Expr := do
  let type ← whnf (← inferType e)
  let .const structName us := type.getAppFn | throwError "{e} doesn't have a structure as type"
  let some projName := getProjFnForField? (← getEnv) structName fieldName |
    throwError "{structName} doesn't have field {fieldName}"
  return mkAppN (.const projName us) (type.getAppArgs.push e)

Direct projection construction

Informal description

Given an expression `e` whose type is a structure with a field named `fieldName`, the function constructs the projection expression `e.fieldName`. If `e` does not have a structure type or the structure does not contain the specified field, an error is thrown.

Lean.Expr.mkProjection definition

(e : Expr) (fieldName : Name) : MetaM Expr

Full source

/-- If `e` has a structure as type with field `fieldName` (either directly or in a parent
structure), `mkProjection e fieldName` creates the projection expression `e.fieldName` -/
def mkProjection (e : Expr) (fieldName : Name) : MetaM Expr := do
  let .const structName _ := (← whnf (← inferType e)).getAppFn |
    throwError "{e} doesn't have a structure as type"
  let some baseStruct := findField? (← getEnv) structName fieldName |
    throwError "No parent of {structName} has field {fieldName}"
  let mut e := e
  for projName in (getPathToBaseStructure? (← getEnv) baseStruct structName).get! do
    let type ← whnf (← inferType e)
    let .const _structName us := type.getAppFn | throwError "{e} doesn't have a structure as type"
    e := mkAppN (.const projName us) (type.getAppArgs.push e)
  mkDirectProjection e fieldName

Structure field projection construction

Informal description

Given an expression `e` whose type is a structure (either directly or through inheritance) with a field named `fieldName`, this function constructs the projection expression `e.fieldName`. If `e` does not have a structure type or the structure does not contain the specified field (even through inheritance), an error is thrown.

Lean.Expr.reduceProjStruct? definition

(e : Expr) : MetaM (Option Expr)

Full source

/-- If `e` is a projection of the structure constructor, reduce the projection.
Otherwise returns `none`. If this function detects that expression is ill-typed, throws an error.
For example, given `Prod.fst (x, y)`, returns `some x`. -/
def reduceProjStruct? (e : Expr) : MetaM (Option Expr) := do
  let .const cname _ := e.getAppFn | return none
  let some pinfo ← getProjectionFnInfo? cname | return none
  let args := e.getAppArgs
  if ha : args.size = pinfo.numParams + 1 then
    -- The last argument of a projection is the structure.
    let sarg := args[pinfo.numParams]'(ha ▸ pinfo.numParams.lt_succ_self)
    -- Check that the structure is a constructor expression.
    unless sarg.getAppFn.isConstOf pinfo.ctorName do
      return none
    let sfields := sarg.getAppArgs
    -- The ith projection extracts the ith field of the constructor
    let sidx := pinfo.numParams + pinfo.i
    if hs : sidx < sfields.size then
      return some (sfields[sidx]'hs)
    else
      throwError m!"ill-formed expression, {cname} is the {pinfo.i + 1}-th projection function \
        but {sarg} does not have enough arguments"
  else
    return none

Projection reduction for structure constructors

Informal description

Given a Lean expression `e` that represents a projection from a structure constructor, this function attempts to reduce the projection to its corresponding field value. If successful, it returns the reduced expression; otherwise, it returns `none`. If the expression is ill-typed (e.g., the projection function does not match the structure constructor or the structure does not have enough fields), an error is thrown. For example, applying this function to `Prod.fst (x, y)` would return `some x`.

Lean.Expr.containsConst definition

(e : Expr) (p : Name → Bool) : Bool

Full source

/-- Returns true if `e` contains a name `n` where `p n` is true. -/
def containsConst (e : Expr) (p : Name → Bool) : Bool :=
  Option.isSome <| e.find? fun | .const n _ => p n | _ => false

Expression contains constant satisfying predicate

Informal description

The function checks whether an expression `e` contains a constant name `n` that satisfies a given predicate `p`. It returns `true` if such a name exists in `e`, and `false` otherwise.

Lean.Expr.rewrite definition

(e eq : Expr) : MetaM Expr

Full source

/--
Rewrites `e` via some `eq`, producing a proof `e = e'` for some `e'`.

Rewrites with a fresh metavariable as the ambient goal.
Fails if the rewrite produces any subgoals.
-/
def rewrite (e eq : Expr) : MetaM Expr := do
  let ⟨_, eq', []⟩ ← (← mkFreshExprMVar none).mvarId!.rewrite e eq
    | throwError "Expr.rewrite may not produce subgoals."
  return eq'

Expression Rewriting with Equality

Informal description

The function `Lean.Expr.rewrite` takes two expressions `e` and `eq` and returns a proof that `e` is equal to some expression `e'` obtained by rewriting `e` using the equality `eq`. The rewrite is performed in a context with a fresh metavariable as the ambient goal, and it fails if the rewrite produces any subgoals.

Lean.Expr.rewriteType definition

(e eq : Expr) : MetaM Expr

Full source

/--
Rewrites the type of `e` via some `eq`, then moves `e` into the new type via `Eq.mp`.

Rewrites with a fresh metavariable as the ambient goal.
Fails if the rewrite produces any subgoals.
-/
def rewriteType (e eq : Expr) : MetaM Expr := do
  mkEqMPmkEqMP (← (← inferType e).rewrite eq) e

Type rewriting via equality

Informal description

The function rewrites the type of an expression `e` using an equality `eq`, then transports `e` to the new type via `Eq.mp`. The rewrite is performed with a fresh metavariable as the ambient goal, and it fails if the rewrite produces any subgoals.

Lean.Expr.forallNot_of_notExists definition

(ex hNotEx : Expr) : MetaM (Expr × Expr)

Full source

/-- Given `(hNotEx : Not ex)` where `ex` is of the form `Exists x, p x`,
return a `forall x, Not (p x)` and a proof for it.

This function handles nested existentials. -/
partial def forallNot_of_notExists (ex hNotEx : Expr) : MetaM (ExprExpr × Expr) := do
  let .app (.app (.const ``Exists [lvl]) A) p := ex | failure
  go lvl A p hNotEx
where
  /-- Given `(hNotEx : Not (@Exists.{lvl} A p))`,
      return a `forall x, Not (p x)` and a proof for it.

      This function handles nested existentials. -/
  go (lvl : Level) (A p hNotEx : Expr) : MetaM (ExprExpr × Expr) := do
    let xn ← mkFreshUserName `x
    withLocalDeclD xn A fun x => do
      let px := p.beta #[x]
      let notPx := mkNot px
      let hAllNotPx := mkApp3 (.const ``forall_not_of_not_exists [lvl]) A p hNotEx
      if let .app (.app (.const ``Exists [lvl']) A') p' := px then
        let hNotPxN ← mkFreshUserName `h
        withLocalDeclD hNotPxN notPx fun hNotPx => do
          let (qx, hQx) ← go lvl' A' p' hNotPx
          let allQx ← mkForallFVars #[x] qx
          let hNotPxImpQx ← mkLambdaFVars #[hNotPx] hQx
          let hAllQx ← mkLambdaFVars #[x] (.app hNotPxImpQx (.app hAllNotPx x))
          return (allQx, hAllQx)
      else
        let allNotPx ← mkForallFVars #[x] notPx
        return (allNotPx, hAllNotPx)

Conversion from ¬∃ to ∀¬ with nested existential handling

Informal description

Given an expression `hNotEx` of type `¬ (∃ x, p x)`, this function constructs an expression of type `∀ x, ¬ (p x)` along with a proof of this statement. The function handles nested existential quantifiers by recursively processing the inner existentials.

Lean.getFieldsToParents definition

(env : Environment) (structName : Name) : Array Name

Full source

/-- Get the projections that are projections to parent structures. Similar to `getParentStructures`,
except that this returns the (last component of the) projection names instead of the parent names.
-/
def getFieldsToParents (env : Environment) (structName : Name) : Array Name :=
  getStructureFields env structName |>.filter fun fieldName =>
    isSubobjectField? env structName fieldName |>.isSome

Projections to parent structures

Informal description

Given an environment `env` and a structure name `structName`, this function retrieves the names of the projection functions that map to parent structures of `structName`. It filters the structure fields to only include those that are subobject fields (i.e., projections to parent structures).