Zulip Chat Archive
Stream: lean4
Topic: Missing `mkCharLit`
Mac (Apr 18 2021 at 20:06):
Any particular reason why Meta.lean
is lacking a mkCharLit
and an instance for Quote Char
?
Last updated: Dec 20 2023 at 11:08 UTC
Any particular reason why Meta.lean
is lacking a mkCharLit
and an instance for Quote Char
?
Last updated: Dec 20 2023 at 11:08 UTC