This used to parse in 8.17 but not in 8.18

```
Coercion foo (b : bool) : nat := if b then 1 else 2.
Check (true = if true then 1 else 2 :> nat).
```

I didn't see anything in the changelog. Why this change?

This topic was moved here from #coq-community devs & users > type cast parsing by Karl Palmskog.

I think this is a question for Coq devs

the introduction of `foo :> bar`

as a cast syntax conflicts with the `x = y :> T`

notation

so now it gets parsed as

```
Check (true = if true then 1 else (2 :> nat)).
```

note that `Check (true = (if true then 1 else 2) :> nat).`

still works

so `Check (true = if true then 1 else 2 :> nat).`

parsing as the equality notation may involve some complicated interaction between the parsing levels of the notation, `if then else`

and the parser's fallback stuff

```
Reserved Notation "x = y :> T"
(at level 70, y at next level, no associativity).
```

`x :> y`

is at level 100 with y at level 200

ifthenelse is at level 200 with subterms at level 200 IIUC

so there is a difference between `(X = (Y :> t))`

and `X = Y :> T`

? Anyway this breaks some of my files, it could be worth mentioning in the CHANGELOG.

In theory, there is no difference. But there is this thing called the parser fallback, which allows Coq to parse things that it should not be allowed to parse if the grammar was respected. Your expression happens to be unparsable (the `if then else`

should have been parenthesized in the first place), so Coq tries harder to parse it, and here the recovery mechanism happens to diverge between 8.17 and 8.18. (I am not saying it should not be documented, just that it falls in the category "erroneous input leads to erroneous behavior".)

I was just wondering why there is still a special notation

```
Reserved Notation "x = y :> T"
```

is it still needed?

ok it seems needed `X = Y :> T`

seems equivalent to `(X :> T) = (Y :> T)`

C'est la notation pour donner explicitement le type d'un `eq`

. (Tu me diras, on aurait peut-être pu choisir quelque chose comme `x =_ A y`

aussi, mais on n'avait pas réalisé à ce moment-là que les notations utilisant `_`

pour évoquer un indice marcheraient aussi bien.)

Last updated: Oct 13 2024 at 01:02 UTC