Stream: math-comp analysis

Topic: ✔ Why does interval type gives me type error?


view this post on Zulip 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?

view this post on Zulip Pierre Roux (Sep 05 2022 at 12:06):

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

view this post on Zulip abab9579 (Sep 06 2022 at 03:04):

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum matrix.
From mathcomp Require Import boolp reals classical_sets signed topology functions.
From mathcomp Require Import prodnormedzmodule normedtype landau forms derive.

Set Implicit Arguments.

Import Order.Theory.
Import GRing.Theory.
Import Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

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

gives the error.

view this post on Zulip Reynald Affeldt (Sep 06 2022 at 03:35):

Maybe add interval to the list of imports.

view this post on Zulip abab9579 (Sep 06 2022 at 03:36):

Thank you, that worked!

view this post on Zulip Notification Bot (Sep 06 2022 at 03:37):

abab9579 has marked this topic as resolved.


Last updated: Jun 22 2024 at 16:02 UTC