rationals

Type Members

1. class Fractions extends Theory with RingWithDivision

   

   The theory of fractions s / t, with s, t taken from some ring.

   The theory of fractions s / t, with s, t taken from some ring. The theory uses an encoding in which the same (fixed, but arbitrary) denominator is used for all expressions. The range of considered denominators is described by the denomConstraint argument over the variable _0.

2. class OrderedFractions extends Fractions with OrderedRing

   

   The theory of fractions s / t, with s, t taken from some ordered ring.

   The theory of fractions s / t, with s, t taken from some ordered ring.