Zulip Chat Archive

Stream: new members

Topic: What does `‹_›` mean?


view this post on Zulip 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).

view this post on Zulip Reid Barton (Oct 02 2020 at 12:20):

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

view this post on Zulip Scott Morrison (Oct 02 2020 at 12:20):

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

view this post on Zulip Eric Wieser (Oct 02 2020 at 12:27):

Where does this notation come from?

view this post on Zulip Eric Wieser (Oct 02 2020 at 12:28):

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

view this post on Zulip Scott Morrison (Oct 02 2020 at 12:28):

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

view this post on Zulip 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