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

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?
How to mix sections with hints in Coq?
Non-trivial Fixpoint on nested recursive types
Is there an intuitionistic proof of `(A -> B \/ C) -> (A -> B) \/ (A -> C)`?
InteractionTrees library - simple program on ASM
What is the difference between Lemma and Theorem in Coq
How to instruct `auto` to simplify the goal during proof search?
Is is possible to rename a coq term?
What are the practical limitations of a non-turing complete language like Coq?
Coq : mutually recursive definitions with [mrec] in InteractionTrees Library
Is there a function that returns a list of values with specific type in OCaml?
Formualting a logic in farmer astronaught
What's the correct setup for Kami (Coq framework for Bluespec) to be able to run on WSL Ubuntu?
Coq: keeping information in a match statement
Showing polynomial equality in coq/ssreflect
Syntax of the case tactic in coq
Understanding nat_ind2 in Logical Foundations
Split multiple conjuncts in the goal
What `dependent induction` tactic does in Coq and how to use it
Coq can't define an inductive proposition
The `specialize` tatic in Coq does not work well with typeclasses?