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.instance not produced anymore #442

Open
affeldt-aist opened this issue Sep 6, 2024 · 0 comments
Open

HB.instance not produced anymore #442

affeldt-aist opened this issue Sep 6, 2024 · 0 comments
Labels

Comments

@affeldt-aist
Copy link
Member

affeldt-aist commented Sep 6, 2024

The following branch

https://github.com/affeldt-aist/analysis/tree/evt2_HB_bug_report_20240906b

records a potential issue with HB.

In normedtype.v, we have changed the definition of the
structure NormedModule so that instead of using GRing.Lmodule
it uses Tvs, which is a structure that includes GRing.Lmodule.

We were expecting that compilation would not fail but a bit later
in the file the command

#[export, non_forgetful_inheritance]
HB.instance Definition _ := NormedModule.copy R R^o.

normedtype.v:849 fails with the following message

Error:
Definition illtyped: In environment
R : realType
The term "Phant R^o" has type "phant (GRing.regular (Real.sort R))"
while it is expected to have type "phant (@NormedModule.sort ?t0 ?t1)".

--

The problem can be circumvented by uncommenting l.811--l.827.
The problem seems to be that the command

HB.instance Definition _ :=
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R R^o (@normrM _).

was not producing an instance anymore and that might reveal
an HB insufficiency to identify instances of mixins.

@mkerjean @CohenCyril

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants