Stream: new members
Topic: What does `‹_›` mean?
Eric Wieser (Oct 02 2020 at 12:13):
‹_› is not to be confused with
Mathlib uses this in a few places: https://github.com/leanprover-community/mathlib/search?q=%E2%80%B9_%E2%80%BA
Figured I'd ask on zulip so that at least someone can search for this in future (assuming zulip search supports these characters).
Reid Barton (Oct 02 2020 at 12:20):
‹t› means something like
show t, by assumption and so
‹_› basically means
Scott Morrison (Oct 02 2020 at 12:20):
‹X› is the same as
(by assumption : X).
Eric Wieser (Oct 02 2020 at 12:27):
Where does this notation come from?
Eric Wieser (Oct 02 2020 at 12:28):
Is it part of the language itself, or a
notation somewhere I can't find?
Scott Morrison (Oct 02 2020 at 12:28):
I think it's baked into the C++.
Rob Lewis (Oct 02 2020 at 12:31):
Last updated: May 13 2021 at 00:41 UTC