Stream: Coq devs & plugin devs

Topic: What is the `Arith.Bool_nat` file for?


view this post on Zulip Pierre Rousselin (Jan 16 2024 at 14:31):

I am very curious about Arith.Bool_nat. It's not required anywhere. What is it used for?

view this post on Zulip Karl Palmskog (Jan 16 2024 at 14:33):

pretty common that Stdlib comprehension is going to require digital archeology. Your best bet might be to search the legacy Coq-contribs for Bool_nat: https://github.com/coq-contribs/

view this post on Zulip Karl Palmskog (Jan 16 2024 at 14:44):

for context, contribs contain probably a majority of all noteworthy Coq code written 1998-2011 or similar.

view this post on Zulip Gaëtan Gilbert (Jan 16 2024 at 15:18):

you can also search all github https://github.com/search?q=%22Bool_nat%22+language%3ACoq&type=code&l=Coq

view this post on Zulip Pierre Rousselin (Jan 23 2024 at 15:13):

I propose to deprecate it : https://github.com/coq/coq/pull/18538
One less file to take care of is still a little win.


Last updated: Oct 13 2024 at 01:02 UTC