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:
NBits
inside PeanoNat.Nat
(without breaking too many things)weird
Sounds like a bug in Search
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.
It's indeed a Search
bug, the lemmas are there.
Done: https://github.com/coq/coq/issues/18657
Last updated: Oct 13 2024 at 01:02 UTC