Takafumi Saikawa
Takafumi Saikawa
> As an aside, today I was quite surprised to learn that "almost everywhere convergence" is [not topological](http://ordman.net/MathResearch/1966A.pdf). So while it looks like we could define a "filteredType" for it,...
It compiles on my machine with coq-8.17.0, mathcomp-1.17.0, analysis-0.6.3, infotheo-0.5.2.
let me temporarily Set Printing All just before the erroneous Equations line
``` Error: - Error: Missing universe constraint declared for inductive type: - Type@{max(Set,mathcomp.ssreflect.tuple.380,MonadAlt.axioms_.u0,monae.fail_lib.5368)}
Confirmed locally that it fails with coq-8.17.1, elpi-1.18.0, and HB-1.6.0. Trying to check further with coq-8.18, elpi-1.19, HB-1.6.0. elpi versions may matter; I have just noticed elpi-1.17.1 + HB-1.6.0 fails...
The same error with coq-8.18.0 + elpi-1.19.0 + HB-1.6.0. (btw, infotheo compiled without a problem with these)
HB 1.4.0 succeeds to compile monae master and HB-1.6.0 fails, regardless of the versions of elpi used. HB 1.6.0 + elpi 1.18 succeeds to compile mathcomp-analysis 0.6.4 and HB 1.6.0...
Oh I have just noticed coq-elpi and elpi are different packages. The versions so far I wrote about elpi was of coq-elpi.
Is it difficult to modify the notation on the LHS to `[_, +oo[ to be consistent?