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).

What is the difference between Lemma and Theorem in Coq
Coq Error Syntax error: '.' expected after [gallina] (in [vernac_aux])
Dependent Pair Types
I'm having difficulty definining a property in Coq, not sure how to approach
Coq is reusing a term in Induction Hypothesis, instead of creating a fresh one
How to prove theorems about mutual inductive types by using tactics in Coq?
Efficient Record Construction in Coq: Is Direct Proof Inclusion Possible?
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?