Documentation

Qq.MetaM

Qq-ified spellings of functions in Lean.Meta #

This file provides variants of the function in the Lean.Meta namespace, which operate with Q(_) instead of Expr.

Equations
Instances For
    def Qq.withLocalDeclDQ {n : TypeType u_1} {u : Lean.Level} {α : Type} [Monad n] [MonadControlT Lean.MetaM n] (name : Lean.Name) (β : Q(Sort u)) (k : Q(«$β»)n α) :
    n α
    Equations
    Instances For
      def Qq.withLocalDeclQ {n : TypeType u_1} {u : Lean.Level} {α : Type} [Monad n] [MonadControlT Lean.MetaM n] (name : Lean.Name) (bi : Lean.BinderInfo) (β : Q(Sort u)) (k : Q(«$β»)n α) :
      n α
      Equations
      Instances For
        def Qq.synthInstanceQ {u : Lean.Level} (α : Q(Sort u)) :
        Lean.MetaM Q(«$α»)
        Equations
        Instances For
          def Qq.instantiateMVarsQ {u : Lean.Level} {α : Q(Sort u)} (e : Q(«$α»)) :
          Lean.MetaM Q(«$α»)
          Equations
          Instances For
            def Qq.elabTermEnsuringTypeQ {u : Lean.Level} (stx : Lean.Syntax) (expectedType : Q(Sort u)) (catchExPostpone : optParam Bool true) (implicitLambda : optParam Bool true) (errorMsgHeader? : optParam (Option String) none) :
            Lean.Elab.TermElabM Q(«$expectedType»)
            Equations
            Instances For
              def Qq.inferTypeQ (e : Lean.Expr) :
              Lean.MetaM ((u : Lean.Level) × (α : let u := u; Q(Sort u)) × Q(«$α»))

              A Qq-ified version of Lean.Meta.inferType

              Instead of writing let α ← inferType e, this allows writing let ⟨u, α, e⟩ ← inferTypeQ e, which results in a context of

              e✝ : Expr
              u : Level
              α : Q(Type u)
              e : Q($α)
              

              Here, the new e is defeq to the old one, but now has Qq-ascribed type information.

              This is frequently useful when using the ~q matching from QQ/Match.lean, as it allows an Expr to be turned into something that can be matched upon.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Qq.checkTypeQ {u : Lean.Level} (e : Lean.Expr) (ty : let u := u; Q(Sort u)) :
                Lean.MetaM (Option Q(«$ty»))

                If e is a ty, then view it as a term of Q($ty).

                Equations
                Instances For
                  inductive Qq.MaybeDefEq {u : Lean.Level} {α : let u := u; Q(Sort u)} (a : Q(«$α»)) (b : Q(«$α»)) :

                  The result of Qq.isDefEqQ; MaybeDefEq a b is an optional version of $a =Q $b.

                  Instances For
                    instance Qq.instReprMaybeDefEq :
                    {u : Lean.Level} → {α : let u := u; Q(Sort u)} → {a b : Q(«$α»)} → Repr (Qq.MaybeDefEq a b)
                    Equations
                    • One or more equations did not get rendered due to their size.
                    def Qq.isDefEqQ {u : Lean.Level} {α : let u := u; Q(Sort u)} (a : Q(«$α»)) (b : Q(«$α»)) :

                    A version of Lean.Meta.isDefEq which returns a strongly-typed witness rather than a bool.

                    Equations
                    Instances For
                      def Qq.assertDefEqQ {u : Lean.Level} {α : let u := u; Q(Sort u)} (a : Q(«$α»)) (b : Q(«$α»)) :
                      Lean.MetaM (PLift («$a» =Q «$b»))

                      Like Qq.isDefEqQ, but throws an error if not defeq.

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