Zulip Chat Archive
Stream: lean4
Topic: Name -> Syntax
Scott Morrison (Dec 01 2021 at 08:21):
Location
recently changed to take an Array Syntax
rather than an Array Name
. If I already have a Name
and want to construct a Location
, how do I turn that Name
back into a Syntax
?
Mario Carneiro (Dec 01 2021 at 08:23):
mkIdent
Last updated: May 02 2025 at 03:31 UTC