Documentation

Qq.Delab

source
opaque Qq.Impl.pp.qq :
Lean.Option Bool
source
def Qq.Impl.checkQqDelabOptions :
Lean.PrettyPrinter.Delaborator.DelabM Unit
Instances For
    source
    instance Qq.Impl.instMonadLiftUnquoteMStateTUnquoteStateDelabM :
    MonadLift Qq.Impl.UnquoteM (StateT Qq.Impl.UnquoteState Lean.PrettyPrinter.Delaborator.DelabM)
    source
    def Qq.Impl.delabQuoted :
    StateT Qq.Impl.UnquoteState Lean.PrettyPrinter.Delaborator.DelabM Lean.Term
    Instances For
      source
      def Qq.Impl.withDelabQuoted (k : StateT Qq.Impl.UnquoteState Lean.PrettyPrinter.Delaborator.DelabM Lean.Term) :
      Lean.PrettyPrinter.Delaborator.Delab
      Instances For
        source
        def Qq.Impl.delabQuotedLevel :
        Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax.Level
        Instances For
          source
          def Qq.Impl.delabQ :
          Lean.PrettyPrinter.Delaborator.Delab
          Instances For
            source
            def Qq.Impl.delabq :
            Lean.PrettyPrinter.Delaborator.Delab
            Instances For
              source
              def Qq.Impl.delabQuotedDefEq :
              Lean.PrettyPrinter.Delaborator.Delab
              Instances For
                source
                def Qq.Impl.delabQuotedLevelDefEq :
                Lean.PrettyPrinter.Delaborator.Delab
                Instances For