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