Stream: math-comp analysis

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

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: Jan 30 2023 at 11:03 UTC