| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Rational
Contents
Description
Symbolic rationals, corresponds to Haskell's Rational type
Constructing rationals
(.%) :: SInteger -> SInteger -> SRational infixl 7 Source #
Construct a symbolic rational from a given numerator and denominator. Note that it is not possible to deconstruct a rational by taking numerator and denominator fields, since we do not represent them canonically. (This is due to the fact that SMTLib has no functions to compute the GCD. One can use the maximization engine to compute the GCD of numbers, but not as a function.)