New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

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

Jump to bottom

A few small improvements to the template tutorial #47

Merged

thomas-lamiaux merged 1 commit into coq:main from MevenBertrand:cleaner_template

Sep 2, 2024

Contributor

MevenBertrand commented Sep 2, 2024

correction of a typo in a Coq definition (missed because the definition is Failed, but it failed by not finding the name, not because of universe constraints)
reformulated "structurally smaller" into simply "smaller": in my book, structurally is usually used when discussing inductive types (see the Equations tutorial for instance), and so using it here feels needlessly confusing
a few extra rephrasing


          a few small improvements to the template tutorial

a10e121

MevenBertrand requested a review from thomas-lamiaux

September 2, 2024 14:38

thomas-lamiaux merged commit 8e8f6b1 into coq:main

2 checks passed

MevenBertrand deleted the cleaner_template branch

September 2, 2024 15:48

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet