We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
I found that the eqnP proof on p. 103 of the book version 1.0.2 differs from the actual Coq result.
The book describes the result after apply: (iffP idP). as follows.
apply: (iffP idP).
n : nat m : nat =================== m = n -> eqn m n subgoal 2 is: eqn m n -> m = n
But Coq actually shows as follows.
n, m : nat ============================ eqn n m -> n = m goal 2 is: n = m -> eqn n m
The order of subgoals is reversed.
The text was updated successfully, but these errors were encountered:
Thanks for sumitting the issue!
Sorry, something went wrong.
Update chSpecification.tex
e547e79
Fix #146
Successfully merging a pull request may close this issue.
I found that the eqnP proof on p. 103 of the book version 1.0.2 differs from the actual Coq result.
The book describes the result after
apply: (iffP idP).
as follows.But Coq actually shows as follows.
The order of subgoals is reversed.
The text was updated successfully, but these errors were encountered: