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