Hi everyone:

I am designing some functions about R type in the Coq standard library Coq.Reals.

I’m so sad that I can’t find/write a function to calculate equality of two Real numbers.

code detail (under Coq 8.13):

From Coq Require Import Reals RMicromega RingMicromega.

Open Scope R_scope.

(* find any boolearn function *)
Search (R → R → bool). (* found this:

Reval_bop2: Op2 → R → R → bool

*)

Eval compute in Reval_bop2 OpEq R1 R1. (*

= if Req_EM_T R1 R1 then true else false

: bool *)

Eval compute in Reval_bop2 OpEq 1 2. (*

= if Req_EM_T R1 (R1 + R1) then true else false

: bool *)

so, I cannot get a boolean result. I only get an expression! but this is too long.

If anybody could help me, or could explain why Coq refused to calculate the boolean result?

Thank you very much!