Get info

Stream: lean4

[Marcus Rossel]

Is there a way to obtain the message data logged with logInfo from another tactic? That is, something like observingLogInfo in the following example:

import Lean
open Lean Meta Elab Term Tactic

elab "log_to_warn" t:tactic : tactic => do
  let msg : MessageData ← observingLogInfo (evalTactic t)
  logWarning msg

[Edward van de Meent]

i think if you look into how #guard_msgs works, you might find such functionality...