What does `‹_›` mean?

Stream: new members

[Eric Wieser]

(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]

‹t› means something likeshow t, by assumption and so ‹_› basically means by assumption.

[Scott Morrison]

In general, ‹X› is the same as (by assumption : X).

[Eric Wieser]

Where does this notation come from?

[Eric Wieser]

Is it part of the language itself, or a notation somewhere I can't find?

[Scott Morrison]

I think it's baked into the C++.

[Rob Lewis]

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