## Stream: general

### Topic: a

#### 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?

#### Reid Barton (Oct 22 2018 at 23:31):

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

#### Mario Carneiro (Oct 22 2018 at 23:37):

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

Whaaaat

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