Comments (4)
CohenCyril
commented on July 19, 2024
1
"owned" by HB, and
eqTypeis notFor completeness, we are working on porting mathcomp to HB.
Yes, cf #100 (comment)
from hierarchy-builder.
CohenCyril
commented on July 19, 2024
Unfortunately as in #100 it is not possible to mix a hierarchy designed independently of HB with one designed in HB. One main purpose of HB itself is to automatically complete missing unification hints (such as the one you encounter here) but in a framework were every single structure is "owned" by HB, and eqType is not, HB does not know it has to add a coercion from my.sort to Equality.sort among other stuff.
Sorry for the inconvenience.
from hierarchy-builder.
CohenCyril
commented on July 19, 2024
Also, I can't make a new Canonical instance for
my.typebecause it conflicts withhb_eqMixin.
As a side note: @EqMixin does not have type eqType but Equality.mixin it is not desirable to make it canonical anyway. You might make it a definition and continue with a Canonical porder_eqType := ... line successfully.
from hierarchy-builder.
gares
commented on July 19, 2024
"owned" by HB, and
eqTypeis not
For completeness, we are working on porting mathcomp to HB.
from hierarchy-builder.
Related Issues (20)
- `HB.howto` fails to inform the user about smart factories HOT 1
- HB fails to infer and to warn properly about missing type information HOT 3
- `HB.about factory` (or a new command e.g. `HB.print`) should give a complete definition of the record.
- `HB.howto stuff` fails sometimes HOT 1
- `HB.howto Stuff.type` fails on structure types with attribute `#[infer...]`
- Provide a way to give names to canonical instances HOT 4
- Define an identity coercion from `type` -> `type_`
- Generated documentation (via coqdoc) has broken links
- Renaming the on notation HOT 3
- HB.about lists the fields in a random order
- Store types with a CS instance in Elpi's Db
- Retrieve types with CS instances from Db
- New command HB.saturate_instances
- Automatic saturation at structure declaration
- Handle types with parameters in automatic saturation HOT 1
- HB.instance with a better complexity
- Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 HOT 1
- HB.pack should hide the class HOT 1
- HB should try to give a fresh name here
- Distinguish instance parameter from mixin parameter
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from hierarchy-builder.