Documentation

Qq.Macro

Instances For
    @[inline, reducible]
    abbrev Qq.Impl.UnquoteM (α : Type) :
    Instances For
      @[inline, reducible]
      abbrev Qq.Impl.QuoteM (α : Type) :
      Instances For
        def Qq.Impl.withUnquotedLCtx {m : TypeType u_1} {α : Type} [MonadControlT Lean.MetaM m] [Monad m] [MonadLiftT Qq.Impl.QuoteM m] (k : m α) :
        m α
        Instances For
          Instances For
            @[inline]
            Equations
            Instances For
              Equations
              Instances For
                @[specialize #[]]
                def Qq.withProcessPostponed {m : TypeType u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT Lean.MetaM m] (k : m α) :
                m α
                Instances For

                  ql(u) quotes the universe level u.

                  Instances For

                    a =QL b says that the levels a and b are definitionally equal.

                    Instances For
                      Instances For

                        q(t) quotes the Lean expression t into a Q(α) (if t : α)

                        Instances For

                          Q(α) is the type of Lean expressions having type α.

                          Instances For

                            a =Q b says that a and b are definitionally equal.

                            Instances For