Stream: Coq devs & plugin devs

Topic: What happens when a module ends?


view this post on Zulip Pierre Rousselin (Feb 06 2024 at 17:27):

I'm confused (again, and probably not for the last time) by modules. In PeanoNat, just before End Nat., Search "land" gives almost nothing, after End Nat. it's different.

Can someone please help me:

  1. understand what is happening
  2. use lemmas in NBits inside PeanoNat.Nat (without breaking too many things)
    ?

view this post on Zulip Gaëtan Gilbert (Feb 06 2024 at 19:26):

weird

view this post on Zulip Jason Gross (Feb 07 2024 at 23:12):

Sounds like a bug in Search

view this post on Zulip Pierre Rousselin (Feb 09 2024 at 08:48):

This is real and quite nasty. I'm trying to modify some files in Numbers and I'm completely in the dark. I'll try to find a minimal example and open an issue.

view this post on Zulip Pierre Rousselin (Feb 09 2024 at 08:49):

It's indeed a Search bug, the lemmas are there.

view this post on Zulip Pierre Rousselin (Feb 10 2024 at 16:41):

Done: https://github.com/coq/coq/issues/18657


Last updated: Oct 13 2024 at 01:02 UTC