Stream: Hierarchy Builder devs & users

Topic: input has no global reference


view this post on Zulip Quentin VERMANDE (Jun 14 2023 at 15:44):

Hello. While messing around with HB, I had the following error : "term->gref: input has no global reference" (see attached file). I am using coq 8.17.0 with HB 1.4.0 and mathcomp 2.0.0. Can someone tell me what this means ?
reltype_minimal.v

view this post on Zulip Enrico Tassi (Jun 14 2023 at 15:59):

The error message is surely perfectible, please open an issue.
I think the problem is that the subject of your instance, id, is not a named term, but rather a notation for fun x => x.
Try idfun (IIRC that is the definition for the identity).

view this post on Zulip Quentin VERMANDE (Jun 14 2023 at 16:05):

Perfect, many thanks.


Last updated: Apr 21 2024 at 01:02 UTC