search

math-comp / mcb

Mathematical Components (the Book)
Other
139 stars 25 forks source link

Fix invalid variable name, so that example code compiles #111

Closed WojciechKarpiel closed 3 years ago

WojciechKarpiel commented 3 years ago

Hello!

Example of inductive specs at chapter 5 uses variable named n in the hypothesis, but refers to m in the proof (ubnPgeq m). I changed n to m and not the other way around, because it gives nicer output (Coq 8.13.0, Mathcomp 1.12.0). When variable is m: forall n : nat, n <= m -> G n When variable is n: forall n0 : nat, n0 <= n -> G n0

gares commented 3 years ago

thanks!