sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Data.SBV.Rational

Contents

- Constructing rationals

Description

Symbolic rationals, corresponds to Haskell's `Rational` type

Synopsis

- (.%) :: SInteger -> SInteger -> SRational

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