Hello,

It looks to me like it is some kind of problem in Coq or in its base libraries.

I'm reading Mathematical Components book. There is an example on page 103:

```
Lemma eqnP {n m : nat} : reflect (n = m) (eqn n m).
Proof.
apply: (iffP idP).
```

after the `apply: (iffP idP).`

I have the next goal

```
n, m : nat
============================
?Goal -> reflect (n = m) (eqn n m)
```

while acording to the book I should have this one:

```
n : nat
m : nat
===================
m = n -> eqn m n
```

It looks to me like system loses the information.

2 questions:

1) Is there a way to solve the goal?

2) Is this a new behavior of system or some kind of bug?

```
$ coqc -v
The Coq Proof Assistant, version 8.13.2 (April 2021)
compiled on Apr 15 2021 14:21:12 with OCaml 4.08.1
```

You probably have some wrong settings. It is your entire file?

You are right.

when placed to dedicated file it works as expected

thank you :)

Last updated: Oct 13 2024 at 01:02 UTC