Documentation

Qq.Delab

Delaborators for q() and Q() notation #

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