Zulip Chat Archive

Stream: general

Topic: a


view this post on Zulip Reid Barton (Oct 22 2018 at 23:31):

Apparently p -> q is syntax for \Pi (a : p), q, including binding a in q? How did I never notice this before?

view this post on Zulip Reid Barton (Oct 22 2018 at 23:31):

Now I understand why Patrick used to complain about variables named a...

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:37):

This is only true inside tactics. In term mode the variable is called _x I think

view this post on Zulip Reid Barton (Oct 22 2018 at 23:38):

Whaaaat

view this post on Zulip Mario Carneiro (Oct 22 2018 at 23:38):

but it is smart and doesn't bind _x in the rhs


Last updated: May 16 2021 at 05:21 UTC