Documentation

Mathlib.Lean.Meta.Basic

Additions to Lean.Meta.Basic #

Likely these already exist somewhere. Pointers welcome.

Restore the metavariable context after execution.

Equations
Instances For

    This function is similar to forallMetaTelescopeReducing: Given e of the form forall ..xs, A, this combinator will create a new metavariable for each x in xs until it reaches an x whose type is defeq to t, and instantiate A with these, while also reducing A if needed. It uses forallMetaTelescopeReducing.

    This function returns a triple (mvs, bis, out) where

    • mvs is an array containing the new metavariables.
    • bis is an array containing the binder infos for the mvs.
    • out is e but instantiated with the mvs.
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[inline]

      pureIsDefEq e₁ e₂ is short for withNewMCtxDepth <| isDefEq e₁ e₂. Determines whether two expressions are definitionally equal to each other when metavariables are not assignable.

      Equations
      Instances For

        mkRel n lhs rhs is mkAppM n #[lhs, rhs], but with optimizations for Eq and Iff.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For