a

Stream: general

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

Whaaaat

[Mario Carneiro]

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