Karl Palmskog (Aug 18 2020 at 20:57): Karl Palmskog (Aug 18 2020 at 20:57):I tried a bunch of different requires, scopes, etc., but is it currently at all supported to get the usual infix notations for the boolean versions of the comparison operators on R, like how ssrnat gives you the boolean ones for nat? For example:
Variable r1 r2 : R.
Check r1 <= r2.
(*
should show:
r1 <= r2 : bool
as opposed to:
r1 <= r2 : Prop
*)
Since I seldom deal directly with Reals in mathcomp-analysis, I have no default recipe but for example the following has type bool:
Require Import Rstruct.
Check Rdefinitions.R0 <= Rdefinitions.R1.
(* Rdefinitions.RbaseSymbolsImpl.R0 <= Rdefinitions.RbaseSymbolsImpl.R1
: bool *)
Or this:
Require Import Rstruct.
Check (0 <= 1 :> Rdefinitions.R).
(* (0 : Rdefinitions.RbaseSymbolsImpl.R) <= (1 : Rdefinitions.RbaseSymbolsImpl.R)
: bool *)
Or this:
Require Import Reals.
Require Import Rstruct.
Check (0 <= 1 :> R).
(* (0 : R) <= (1 : R)
: bool *)
(let's say in a context that Require Import the files up to normedtype.v)
Karl Palmskog (Aug 18 2020 at 23:56):hmm, so like this?
From Coq Require Import Reals.
From mathcomp.analysis Require Import
boolp ereal reals posnum landau classical_sets Rstruct Rbar topology prodnormedzmodule normedtype.
(*
this gives using release 0.3.2:
Error:
Level 2 is already declared right associative while it is now expected to be left associative.
*)
Maybe insert this in-between:
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum.
(only the first line is sufficient to get rid of the error)
Karl Palmskog (Aug 19 2020 at 00:25):I may be missing something:
From Coq Require Import Reals.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum.
From mathcomp.analysis Require Import
boolp ereal reals posnum landau classical_sets Rstruct Rbar topology prodnormedzmodule normedtype.
Fail Check (0 <= 1 :> Rdefinitions.R). (* Unknown interpretation for notation "_ <= _ :> _". *)
Fail Check (0 <= 1 :> R). (* Unknown interpretation for notation "_ <= _ :> _". *)
Local Open Scope ring_scope. before the Checks
Reynald Affeldt (Aug 19 2020 at 00:35):(with my apologies: I should have prepared a minimal example from the start but I was not in a working environment)
Last updated: Apr 18 2024 at 23:01 UTC