Pierre Castéran (Jan 06 2023 at 10:17): Pierre Castéran (Jan 06 2023 at 10:17):I don't understand this warning (https://github.com/coq-community/hydra-battles/pull/141/files#annotation_7650253389 )
Function zero (n:nat) {wf lt n} : nat :=
match n with
0 => 0
| p => zero (Nat.div2 p)
Check warning on line 9 in theories/ordinals/Prelude/Fuel.v
GitHub Actions / build (mathcomp/mathcomp-dev:coq-dev)
Unused variable p might be a misspelled constructor. Use _ or _p to
Check warning on line 9 in theories/ordinals/Prelude/Fuel.v
GitHub Actions / build (mathcomp/mathcomp-dev:coq-dev)
Unused variable p0 might be a misspelled constructor. Use _ or _p0
end.
Perhaps a bug in Function? or an old not-removed warning?
Karl Palmskog (Jan 06 2023 at 11:01):the idea is that Coq can't know if you're trying to write a constructor or variable. I think the proper way to write this is:
Function zero (n:nat) {wf lt n} : nat :=
match n with
0 => 0
| S n' as p => zero (Nat.div2 p)
end.
You don't even need n' in there btw.
Karl Palmskog (Jan 07 2023 at 21:40):aesthetically and practically, do you really think S _ as p is better and more readable? I think it's a good idea to generally use n for top-level nat arguments and n' for their subterms.
Pierre Castéran (Jan 08 2023 at 07:28):Or something like Ssr’s is S syntax?
Btw, I’m now trying to improve readability of scripts from Ackermann/Goedel files.
It’s a long, slow, but interesting task…
Last updated: Jun 10 2023 at 23:01 UTC