Stream: math-comp analysis

Topic: Why does interval type gives me type error?

abab9579 (Sep 03 2022 at 01:29):

Basically, when I opened classical_scope, then did

Section Foo.
Context (R: realType).
Check (`[0: R, 1: R]).
End Foo.

I get the following error:

The term
 "interval.Interval (interval.BSide true (0 : R))
    (interval.BSide false (1 : R))" has type "interval.interval R"
while it is expected to have type "pred_sort ?pT".

Adding %classical does not change anything.
Why is this happening?

Pierre Roux (Sep 05 2022 at 12:06):

Please provide more context (imports) otherwise we cannot reproduce.

Last updated: Jan 30 2023 at 10:03 UTC