Zulip Chat Archive

Stream: new members

Topic: What does `‹_›` mean?

Eric Wieser (Oct 02 2020 at 12:13):

(Where ‹_› is not to be confused with <_> or ⟨_⟩)

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 likeshow t, by assumption and so ‹_› basically means by assumption.

Scott Morrison (Oct 02 2020 at 12:20):

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