Coerce rat to realType im math-comp/analysis

Is there a way to coerce a rat into a realType (from the math-comp/analysis library)? For example, the notation for coercing a nat is %:R.

Solution

According to the documentation ratr coerces a rat to any unit ring (hence any realType).

Agda-like programming in Coq/Proof General?
Coq using lemma itself for proof
Pigeonhole proof without decidable equality or excluded middle
Why does Coq solve_in_Union tactic fail directly but works through assertion of identical goal?
How to prove existence in COQ?
How can I prove excluded middle with the given hypothesis (forall P Q : Prop, (P -> Q) -> (~P \/ Q))?
Lemma cannot be used as a hint
Unfolding an opaque fixpoint in Coq
Ltac for deterministic rewriting/sorting of operands
Can I use a tactics under `coqtop -nois`?
What is to be used in place of exfalso omega?
Casting a value from one fintype to another?
How can we use the familiar notation of integer arithmetics in ssreflect?
Stuck at a simple inequality of natural number proof in Coq
Coq - VSCode highlight Compute command in blue
Turn `P(?x)` into `exists x,P(x)` to give different instantiations for different subgoals in Coq
Why doesn't Coq notation defined by other notation working well?
"Cannot guess decreasing argument of fix" error when defining a Fixpoint for extracting the first half of a list
Wrong Typeclass Instance used in Coq Proof
Coq's Search command and modules
How to make OCaml (or Coq) code from the llvmir code using vellvm framework
Coq repeating "destruct" for disjunctive hypothesis causing unwanted destruction in the end
Is there a lightweight way to define a mutable dictionary that can return all of its keys in Coq?
Constructing proof terms inside a recursive function
Coq notation defined inside a module expecting type without module prefix
How does one implement Coq?
Can a dependently typed language be Turing complete?
Beta-reduction after delta-reduction in unfold tactic
Equality for elements of sig type in Coq
Defining mutually recursive types in Coq?