Underlying structure for remarks

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

All remarks in the environment.

Equations

• PhysLean.allRemarkInfo = do let env ← Lean.getEnv pure (PhysLean.remarkExtension.getState env)

def PhysLean.RemarkInfo.toFullName (r : RemarkInfo) : Lean.Name

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

Equations

• r.toFullName = if (r.nameSpace != Lean.Name.anonymous) = true then r.nameSpace.str r.name.toString else r.name

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

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.