Ssreflect Users Discussion List

[Frédéric Chyzak <>]

Next, I played with rat:

Require Import ssralg rat.
Open Scope ring_scope.

Check 1:rat.  (* in rat *)

Check (1:rat) / (3%:R).  (* in rat_Ring *)
Check (1:rat) / (3%:Q).  (* in rat_Ring *)

Check (0:rat) + (Posz 3)%:~R.  (* in rat_ZmodType *)
Check 3%:R:rat.  (* in rat *)
Check 1%:R:rat.

The second and third Check's are the best I could get to speak of 1/3.  Is 
there a direct way to define 1/3 directly in rat?

It seems that the fifth Check is the best I could ge to speak of 3, seen in 
much as possible in rat.  Is there a better/more direct way to define 3 of 
rat?

What is the difference between 1:rat and 1%:R:rat ?

Frédéric