Skip to content

Improve printing functions of TemplateMonad #1118

@MathisBD

Description

@MathisBD

Currently tmPrint always outputs on the "notices" channel. It would be nice if the user could choose the channel. Something like :

Axiom tmMsg : LogLevel.t -> forall {A}, A -> TemplateMonad unit.

Module LogLevel.
Inductive t :=
  | Debug
  | Info 
  | Notice 
  | Warning 
  | Error.
End LogLevel.

And then we could define tmPrint as :

Definition tmPrint := tmMsg Notice.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    Status
    Todo

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions