Zulip Chat Archive

Stream: mathlib4

Topic: print instances

Yury G. Kudryashov (Jan 13 2023 at 03:49):

How do I translate

#print instances nonempty

from Lean 3 to Lean 4?

Last updated: Dec 20 2023 at 11:08 UTC