What do we call (name : type)?

Stream: new members

[Eric Wieser]

What's the name for this syntax, eg (1 : ℤ)? It's not a coercion in this case. Is it a "type ascription"? A "type annotation"? Something else? Or is there no agreed upon name?

[Floris van Doorn]

Type ascription is a common term for it.

[Scott Morrison]

It would also be fair in some cases to call it an "explicit coercion" if the purpose of the type ascription is to trigger a coercion.

[Julian Berman]

Relatedly, I can't find where this syntax is actually defined (in Lean 4), so if anyone knows where that lives, would love to see it. I've looked in the usual places I think (src/Lean/Parser/, src/Init/Notation*.lean)

[Kevin Buzzard]

Are you talking about numerals explicitly or about e.g. (a : Y) when a : X and X = Y? These are two different things, right?

[Eric Wieser]

I think I'm talking about the X = Y case, but there X is really full of metavariables so it seems wrong to equate it to Y

[Mario Carneiro]

Julian Berman said:

Relatedly, I can't find where this syntax is actually defined (in Lean 4), so if anyone knows where that lives, would love to see it. I've looked in the usual places I think (src/Lean/Parser/, src/Init/Notation*.lean)

https://github.com/leanprover/lean4/blob/master/src/Lean/Parser/Term.lean#L67

[Mario Carneiro]

def typeAscription := leading_parser " : " >> termParser

[Mario Carneiro]

which should also answer eric's question

[Mario Carneiro]

The primary effect of a type ascription is to assert that a term has a type; this has the side effect of unifying metavariables and inserting coercions where necessary, so you will usually see it in those contexts, but you can also use it when it has no effect, just to make something clear to the reader.