Why does
Fixpoint k1 n := match n with 0 => 0 | S n => n end
with k2 n := match n with 0 => 0 | S n => n end.
say Well-foundedness check may fail unexpectedly.
?
(since coq#c1b09aec5414b7c18d99029ac091d976ccb179fb cc @Hugo Herbelin )
Gaëtan Gilbert said:
Why does
Fixpoint k1 n := match n with 0 => 0 | S n => n end with k2 n := match n with 0 => 0 | S n => n end.
say
Well-foundedness check may fail unexpectedly.
?
(since coq#c1b09aec5414b7c18d99029ac091d976ccb179fb cc Hugo Herbelin )
I don't remember why I wrote this message. It might finally be clearer to remove it.
Last updated: Oct 13 2024 at 01:02 UTC