sbv-9.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.SBV.Rational

Description

Symbolic rationals, corresponds to Haskell's Rational type

Synopsis

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