Zulip Chat Archive
Stream: mathlib4
Topic: Explicit naming
Jeremy Tan (Mar 18 2023 at 11:35):
@Ruben Van de Velde how do I give an instance an explicit name?
Yaël Dillies (Mar 18 2023 at 11:36):
instance the_name : the_instance_type := the_instance_body
Jeremy Tan (Mar 18 2023 at 11:40):
Yaël Dillies said:
instance the_name : the_instance_type := the_instance_body
Right… I wasn't thinking the first time
Last updated: May 02 2025 at 03:31 UTC