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.trySynthInstanceQ {u : Lean.Level} (α : Q(Sort u)) :
              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 implicitLambda : Bool := true) (errorMsgHeader? : 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
                                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 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($α✝)} :
                                        Equations
                                          def Qq.isDefEqQ {u : Lean.Level} {α : let u := u; Q(Sort u)} (a 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 b : Q(«$α»)) :
                                              Lean.MetaM (PLift («$a» =Q «$b»))

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

                                              Equations
                                                Instances For

                                                  The result of Qq.isLevelDefEqQ; MaybeLevelDefEq u v is an optional version of $u =QL $v.

                                                  Instances For

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

                                                    Equations
                                                      Instances For

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

                                                        Equations
                                                          Instances For