Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
I guess #18601 fixes this issue for `cbn`, no?
In order to merge both this PR and #1166, the preorder structures have to be dualized (See Section 3.3 of https://inria.hal.science/hal-04008820v1/document). I don't have time to deal with the conflict...
@proux01 We need #1166 for our ITP submission. There are still a few things to fix, but I hope it will be ready for review by the end of February.
I cannot promise to rebase #1166 on this PR even if you don't split order.v now, because I really don't know how difficult it will be and I'm not a...
@Tragicus Feel free to ping me if you need help redoing this PR.
> Meanwhile, maybe you can work around it by replacing HB.saturate with some manual HB.instance as done by @pi8027 in its previous semilattive PR, but not sure it's worth the...
@Tragicus Can you push the test with `Fail`? I will take a look.
This PR currently introduces some non-uniform inheritance in the coercion graph. I think the following definitions have to be specialized back to `lmodType` and `lalgType` because the definition of `linear_closed`...
Now, we only have to fix analysis, abel, and a few issues left in the PR. Fixing analysis is nontrivial since it directly uses `Scale.law` in a few places.
I think I need help in fixing analysis.