Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

HB.howto fails with weird error message on mixins, factories and classes. #321

Open
CohenCyril opened this issue Nov 23, 2022 · 0 comments
Labels
easy difficulty Very easy high priority High priority

Comments

@CohenCyril
Copy link
Member

CohenCyril commented Nov 23, 2022

Example:

From Coq Require Import ZArith ssrfun ssreflect.
From HB Require Import structures.
From HB Require Import demo1.hierarchy_5.

Fail HB.howto AddMonoid_of_TYPE. (* mixin *)
Fail HB.howto Ring_of_TYPE. (* factory *)
Fail HB.howto Ring. (* class *)

fails with error

The command has indeed failed with message:
Not Yet Implemented: complex call to Locate: Ring

it is indeed not yet implemented... but not because of locate.

We should either give it a meaning (signature of the mixin / factory and saying using a class can be used only with .on or .copy ?) or fail with an error message pointing towards the structure of interest (here Ring.type when asking about Ring).

See #322 as a starting point for a fix.

@CohenCyril CohenCyril changed the title HB.howto fails with weird error message on mixins, factories and classes. HB.howto fails with weird error message on mixins, factories and classes. Nov 23, 2022
@proux01 proux01 added high priority High priority easy difficulty Very easy labels Dec 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
easy difficulty Very easy high priority High priority
Projects
None yet
Development

No branches or pull requests

2 participants