Documentation

PhysLean.Meta.Remark.Properties

Underlying structure for remarks #

source
def PhysLean.allRemarkInfo {m : Type → Type} [Monad m] [Lean.MonadEnv m] :
m (Array RemarkInfo)

All remarks in the environment.

Equations
    Instances For
      source
      def PhysLean.RemarkInfo.toFullName (r : RemarkInfo) :
      Lean.Name

      The full name of a remark (name and namespace).

      Equations
        Instances For
          source
          def PhysLean.RemarkInfo.IsRemark {m : Type → Type} [Monad m] [Lean.MonadEnv m] (n : Lean.Name) :
          m Bool

          A Bool which is true if a name corresponds to a remark.

          Equations
            Instances For
              source
              def PhysLean.RemarkInfo.getRemarkInfo {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (n : Lean.Name) :
              m RemarkInfo

              Gets the remarkInfo from a name corresponding to a remark..

              Equations
                Instances For