## 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):

https://github.com/leanprover-community/lean/blob/master/library/init/meta/tactic.lean#L1024

Last updated: May 13 2021 at 00:41 UTC