Zulip Chat Archive

Stream: general

Topic: Success message


view this post on Zulip Patrick Massot (Jan 24 2021 at 13:25):

Is there anyone who can make use of the comment at https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive_expr.lean#L402-L408? Copy and pasting those lines seem to do nothing.

view this post on Zulip Rob Lewis (Jan 24 2021 at 13:37):

It works for me -- with this I see my_message instead of Goals accomplished! :tada: at the end of the example.

import tactic.interactive_expr

meta def my_new_msg {α : Type} : widget.html α := "my message"
attribute [vm_override my_new_msg] widget_override.goals_accomplished_message

example : true :=
begin
  trivial,
end

view this post on Zulip Patrick Massot (Jan 24 2021 at 13:58):

Oh, I had too many layers of overrides.

view this post on Zulip Patrick Massot (Jan 24 2021 at 13:58):

Thanks


Last updated: May 10 2021 at 17:39 UTC