Takafumi Saikawa
Takafumi Saikawa
We could also try to incorporate a quaternary definition of the convex combination operator as in (Stone, 1949). The factory for this structure would look like this: ``` HB.factory Record...
@let-def rebasing done. will you test some of your code using this?
Thank you @charguer ! I will add these tests in the testsuite and examine the results.
It seems I have broken something during rebasing, and tests/typing-misc/constraints.ml now segfaults.. I am about to fix this issue.
There have been ghost expressions / patterns in `parser.mly` that use (abuse?) `Pexp_tuple` / `Ppat_tuple` and they now need to be coupled with extra `None`, which looks a bit ugly....
The only essential change in `imonae_lib.v` is the addition of `funeqP`, and it is not necessary for `monae_lib.v` since it is provided by `boolp.v` https://github.com/math-comp/analysis/blob/155492be64984449ebcdd79191ebdf5983fed60c/classical/boolp.v#L147 Do you suggest redefining it...
Porting `Arguments` lines to `monae_lib.v` seems to be harmless.
It think this PR should be anyway turned into a draft. (or perhaps abandoned since the original goal to define functor categories has not been achieved even by impredicativity.)
(I have no idea for the original question, but) Why do you want to specialize the instance to `realType`? `realFieldType` seems to suffice.