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?
Please provide more context (imports) otherwise we cannot reproduce.
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.
Maybe add interval
to the list of imports.
Thank you, that worked!
abab9579 has marked this topic as resolved.
Last updated: Apr 17 2024 at 19:01 UTC