Stream: Coq devs & plugin devs

Topic: Well-foundedness check may fail unexpectedly.


view this post on Zulip Gaëtan Gilbert (Aug 11 2021 at 19:35):

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 )

view this post on Zulip Hugo Herbelin (Aug 19 2021 at 11:07):

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 21 2021 at 22:02 UTC