dvr
Reputation: 370
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.
Upvotes: 0
Views: 44
Answers (1)
Pierre Roux
Reputation: 36
According to the documentation ratr coerces a rat to any unit ring (hence any realType).
Upvotes: 2
Related Questions
- using addf_div for rat_numDomainType
- Case analysis on max - ssreflect
- Coq/SSReflect: standard way to case on (x < y) + (x == y) + (y < x)?
- Translating proof from Nat to Rat
- Coq/SSReflect: How to do case analysis when reflecting && and /\
- Finite list with unknown size
- Cardinality of finFieldType / Euler's criterion
- Is there a convention for the order of applying ssreflect tactic/taticals?
- Extracting integer from int_Ring type in mathcomp's ssralg
- How to introduce a new variable in Coq?