{-# OPTIONS --guardedness #-}

--------------------------------------------------------------------------------
-- Schmitty the Solver
--
-- Exports the `Theory` and `Reflectable` instances for the theory of real
-- numbers, called `theory` and `reflectable`.
-- See <http://smtlib.cs.uiowa.edu/theories-Reals.shtml>.
--------------------------------------------------------------------------------

module SMT.Theories.Reals where

open import SMT.Theories.Reals.Base public
open import SMT.Theories.Reals.Reflection public