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: Dec 20 2023 at 11:08 UTC