has_to_tactic_format

Stream: mathlib4

[Shreyas Srinivas]

What is the lean 4 typeclass that is equivalent to lean3's has_to_tactic_format?

[Eric Wieser]

I think it's merged with docs4#Repr now?

[Shreyas Srinivas]

So can I just delete those extra instances?

[Shreyas Srinivas]

There was a separate instance for has_to_format in the lean3 version and there seems to be a corresponding lean4 typeclass is Std.Format and not Repr

[Eric Wieser]

docs4#Std.Format is not a typeclass. Are you thinking of something else?

[Shreyas Srinivas]

Sorry Std.ToFormat (https://leanprover-community.github.io/mathlib4_docs/Init/Data/Format/Basic.html#Std.ToFormat)

[Notification Bot]

6 messages were moved here from #mathlib4 > Data.Array.Lemmas PR !4#2194 by Eric Wieser.

[Eric Wieser]

Moved for more visibility

[Shreyas Srinivas]

The instances of Repr and Std.ToFormat are doing the exact same thing in this case.

[Shreyas Srinivas]

But the instance of whatever is supposed to replace has_to_tactic_format is calling tactic.pp ∘ toList, instead of format ∘ toList

[Shreyas Srinivas]

I can't find tactic.pp in the lean 4 docs