diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
index c05c8f03a..8c8e1c622 100644
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -52,7 +52,8 @@ primitive type {n : #} (fin n, n >= 1) => Z n : *
 
 /**
  * 'Rational' is the type of rational numbers.
- * Rational numbers form a Field (and thus a Ring).
+ * Rational numbers form a Field (and thus a Ring),
+ * and rational numbers also inhabit the Round class.
  *
  * The 'ratio' operation may be used to directly create
  * rational values from as a ratio of integers, or
@@ -61,6 +62,23 @@ primitive type {n : #} (fin n, n >= 1) => Z n : *
  */
 primitive type Rational : *
 
+/**
+ * 'Real' is the type of real numbers.
+ * Real numbers form a Field (and thus a Ring),
+ * and real numbers also inhabit the Round class.
+ *
+ * For computation purposes, 'Real' is very similar
+ * to 'Rational'.  However, the logical theory of real
+ * numbers admits algebraic numbers in addition to
+ * rationals.  Counterintuitively, solvers may have a
+ * simpler time solving problems involving the real numbers
+ * than similar problems involving the integers or the
+ * rationals because there are dedicated algorithms that
+ * can be applied to real closed fields.
+ */
+primitive type Real : *
+
+
 type Bool = Bit
 type Word n = [n]
 type Char = [8]
@@ -680,6 +698,14 @@ primitive lg2 : {n} (fin n) => [n] -> [n]
 primitive ratio : Integer -> Integer -> Rational
 
 
+// Real specific operations --------------------------------------------------
+
+/**
+ * Compute the real number corresponding to the given rational.
+ */
+primitive fromRational : Rational -> Real
+
+
 // Zn specific operations ----------------------------------------------------
 
 /**
diff --git a/src/Cryptol/Backend.hs b/src/Cryptol/Backend.hs
index 023a3b2e5..abc7ada98 100644
--- a/src/Cryptol/Backend.hs
+++ b/src/Cryptol/Backend.hs
@@ -213,6 +213,7 @@ class MonadIO (SEval sym) => Backend sym where
   type SWord sym :: Type
   type SInteger sym :: Type
   type SFloat sym :: Type
+  type SReal sym :: Type
   type SEval sym :: Type -> Type
 
   -- ==== Evaluation monad operations ====
@@ -281,7 +282,6 @@ class MonadIO (SEval sym) => Backend sym where
   -- | Pretty-print a floating-point value
   ppFloat :: sym -> PPOpts -> SFloat sym -> Doc
 
-
   -- ==== Identifying literal values ====
 
   -- | Determine if this symbolic bit is a boolean literal
@@ -301,6 +301,9 @@ class MonadIO (SEval sym) => Backend sym where
   -- | Determine if this symbolic integer is a literal
   integerAsLit :: sym -> SInteger sym -> Maybe Integer
 
+  -- | Determine if this symbolic real is a literal
+  realAsLit :: sym -> SReal sym -> Maybe Rational
+
   -- ==== Creating literal values ====
 
   -- | Construct a literal bit value from a boolean.
@@ -319,6 +322,12 @@ class MonadIO (SEval sym) => Backend sym where
     Integer {- ^ Value -} ->
     SEval sym (SInteger sym)
 
+  -- | Construct a literal real value from the given rational
+  realLit ::
+    sym ->
+    Rational ->
+    SEval sym (SReal sym)
+
   -- | Construct a floating point value from the given rational.
   fpLit ::
     sym ->
@@ -335,6 +344,7 @@ class MonadIO (SEval sym) => Backend sym where
   iteBit :: sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
   iteWord :: sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
   iteInteger :: sym -> SBit sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
+  iteReal :: sym -> SBit sym -> SReal sym -> SReal sym -> SEval sym (SReal sym)
 
   -- ==== Bit operations ====
   bitEq  :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
@@ -627,6 +637,89 @@ class MonadIO (SEval sym) => Backend sym where
     SInteger sym ->
     SEval sym (SBit sym)
 
+  -- ==== Real operations =====
+
+  intToReal ::
+    sym ->
+    SInteger sym ->
+    SEval sym (SReal sym)
+
+  realPlus ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realNegate ::
+    sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realMinus ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realMult ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realRecip ::
+    sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realDiv ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realEq ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SBit sym)
+
+  realLessThan ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SBit sym)
+
+  realGreaterThan ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SBit sym)
+
+  realFloor ::
+    sym ->
+    SReal sym ->
+    SEval sym (SInteger sym)
+
+  realCeiling ::
+    sym ->
+    SReal sym ->
+    SEval sym (SInteger sym)
+
+  realTrunc ::
+    sym ->
+    SReal sym ->
+    SEval sym (SInteger sym)
+
+  realRoundAway ::
+    sym ->
+    SReal sym ->
+    SEval sym (SInteger sym)
+
+  realRoundToEven ::
+    sym ->
+    SReal sym ->
+    SEval sym (SInteger sym)
 
   -- ==== Operations on Z_n ====
 
diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs
index b653a0d25..d7574ff51 100644
--- a/src/Cryptol/Backend/Concrete.hs
+++ b/src/Cryptol/Backend/Concrete.hs
@@ -134,8 +134,10 @@ instance Backend Concrete where
   type SWord Concrete = BV
   type SInteger Concrete = Integer
   type SFloat Concrete = FP.BF
+  type SReal Concrete = Rational
   type SEval Concrete = Eval
 
+
   raiseError _ err =
     do stk <- getCallStack
        io (X.throwIO (EvalErrorEx stk err))
@@ -186,6 +188,7 @@ instance Backend Concrete where
   iteBit _ b x y  = pure $! if b then x else y
   iteWord _ b x y = pure $! if b then x else y
   iteInteger _ b x y = pure $! if b then x else y
+  iteReal _ b x y = pure $! if b then x else y
 
   wordLit _ w i = pure $! mkBv w i
   wordAsLit _ (BV w i) = Just (w,i)
@@ -309,6 +312,32 @@ instance Backend Concrete where
     do assertSideCondition sym (y /= 0) DivideByZero
        pure $! x `mod` y
 
+  realAsLit _ x = Just x
+  realLit _ x   = pure x
+  intToReal _ x = pure $! (fromInteger x :: Rational)
+  realPlus _ x y  = pure $! x + y
+  realNegate _ x  = pure $! negate x
+  realMinus _ x y = pure $! x - y
+  realMult _ x y  = pure $! x * y
+  realRecip sym x =
+    do assertSideCondition sym (x /= 0) DivideByZero
+       pure $! recip x
+  realDiv sym x y =
+    do assertSideCondition sym (y /= 0) DivideByZero
+       pure $! x / y
+
+  realEq _ x y          = pure $! x == y
+  realLessThan _ x y    = pure $! x < y
+  realGreaterThan _ x y = pure $! x > y
+
+  realFloor _ x       = pure $! floor x
+  realCeiling _ x     = pure $! ceiling x
+  realTrunc _ x       = pure $! truncate x
+  realRoundToEven _ x = pure $! round x
+  realRoundAway _ x
+    | x >= 0    = pure $! floor (x + 0.5)
+    | otherwise = pure $! ceiling (x - 0.5)
+
   intToZn _ 0 _ = evalPanic "intToZn" ["0 modulus not allowed"]
   intToZn _ m x = pure $! x `mod` m
 
diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs
index 78c184374..6a432e8d7 100644
--- a/src/Cryptol/Backend/SBV.hs
+++ b/src/Cryptol/Backend/SBV.hs
@@ -23,6 +23,7 @@ module Cryptol.Backend.SBV
   , freshSBool_
   , freshBV_
   , freshSInteger_
+  , freshSReal_
   , addDefEqn
   , ashr
   , lshr
@@ -37,6 +38,7 @@ import           Control.Concurrent.MVar
 import           Control.Monad.IO.Class (MonadIO(..))
 import           Data.Bits (bit, complement)
 import           Data.List (foldl')
+import           Data.Ratio
 
 import qualified GHC.Integer.GMP.Internals as Integer
 
@@ -94,6 +96,9 @@ freshSInteger_ :: SBV -> IO (SInteger SBV)
 freshSInteger_ (SBV stateVar _) =
   withMVar stateVar (svMkSymVar_ Nothing KUnbounded Nothing)
 
+freshSReal_ :: SBV -> IO (SReal SBV)
+freshSReal_ (SBV stateVar _) =
+  withMVar stateVar (svMkSymVar_ Nothing KReal Nothing)
 
 -- SBV Evaluation monad -------------------------------------------------------
 
@@ -153,6 +158,7 @@ instance Backend SBV where
   type SWord SBV = SVal
   type SInteger SBV = SVal
   type SFloat SBV = ()        -- XXX: not implemented
+  type SReal SBV = SVal
   type SEval SBV = SBVEval
 
   raiseError _ err = SBVEval $
@@ -216,6 +222,7 @@ instance Backend SBV where
   iteBit _ b x y = pure $! svSymbolicMerge KBool True b x y
   iteWord _ b x y = pure $! svSymbolicMerge (kindOf x) True b x y
   iteInteger _ b x y = pure $! svSymbolicMerge KUnbounded True b x y
+  iteReal _ b x y = pure $! svSymbolicMerge KReal True b x y
 
   bitAsLit _ b = svAsBool b
   wordAsLit _ w =
@@ -318,6 +325,32 @@ instance Backend SBV where
        let p = svLessThan z b
        pure $! svSymbolicMerge KUnbounded True p (svRem a b) (svUNeg (svRem (svUNeg a) (svUNeg b)))
 
+  realLit _ q = pure $! svReal q
+  realAsLit _ x =
+    do n <- svNumerator x
+       d <- svDenominator x
+       pure (n % d)
+  intToReal _ i   = pure $! svFromIntegral KReal i
+  realPlus _ x y  = pure $! svPlus x y
+  realNegate _ x  = pure $! SBV.svUNeg x
+  realMinus _ x y = pure $! svMinus x y
+  realMult _ x y  = pure $! svTimes x y
+  realRecip sym x = realDiv sym (svReal 1) x
+  realDiv sym x y =
+    do let z = svReal 0
+       assertSideCondition sym (svNot (svEqual y z)) DivideByZero
+       pure $! svDivide x y
+
+  realEq _ x y          = pure $! svEqual x y
+  realLessThan _ x y    = pure $! svLessThan x y
+  realGreaterThan _ x y = pure $! svGreaterThan x y
+
+  realFloor _ _       = unsupported "real floor"
+  realCeiling _ _     = unsupported "real ceiling"
+  realTrunc _ _       = unsupported "real trunc"
+  realRoundAway _ _   = unsupported "real roundAway"
+  realRoundToEven _ _ = unsupported "real roundToEven"
+
   -- NB, we don't do reduction here
   intToZn _ _m a = pure a
 
diff --git a/src/Cryptol/Backend/What4.hs b/src/Cryptol/Backend/What4.hs
index 1c30726ef..51c1d63a4 100644
--- a/src/Cryptol/Backend/What4.hs
+++ b/src/Cryptol/Backend/What4.hs
@@ -205,13 +205,21 @@ assertIntDivisor sym x =
   do p <- liftIO (W4.notPred (w4 sym) =<< W4.intEq (w4 sym) x =<< W4.intLit (w4 sym) 0)
      assertSideCondition sym p DivideByZero
 
+assertRealDivisor ::
+  W4.IsSymExprBuilder sym => What4 sym -> W4.SymReal sym -> W4Eval sym ()
+assertRealDivisor sym x =
+  do p <- liftIO (W4.notPred (w4 sym) =<< W4.realEq (w4 sym) x =<< W4.realLit (w4 sym) 0)
+     assertSideCondition sym p DivideByZero
+
 instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
   type SBit (What4 sym)     = W4.Pred sym
   type SWord (What4 sym)    = SW.SWord sym
   type SInteger (What4 sym) = W4.SymInteger sym
+  type SReal (What4 sym)    = W4.SymReal sym
   type SFloat (What4 sym)   = FP.SFloat sym
   type SEval (What4 sym)    = W4Eval sym
 
+
   raiseError _ = evalError
 
   assertSideCondition _ cond err
@@ -314,6 +322,7 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
   iteBit sym c x y = liftIO (W4.itePred (w4 sym) c x y)
   iteWord sym c x y = liftIO (SW.bvIte (w4 sym) c x y)
   iteInteger sym c x y = liftIO (W4.intIte (w4 sym) c x y)
+  iteReal sym c x y = liftIO (W4.realIte (w4 sym) c x y)
 
   bitEq  sym x y = liftIO (W4.eqPred (w4 sym) x y)
   bitAnd sym x y = liftIO (W4.andPred (w4 sym) x y)
@@ -425,6 +434,30 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
   intLessThan sym x y = liftIO $ W4.intLt (w4 sym) x y
   intGreaterThan sym x y = liftIO $ W4.intLt (w4 sym) y x
 
+  realAsLit _ x     = W4.asRational x
+  realLit sym x     = liftIO (W4.realLit (w4 sym) x)
+  intToReal sym x   = liftIO (W4.integerToReal (w4 sym) x)
+  realPlus sym x y  = liftIO (W4.realAdd (w4 sym) x y)
+  realNegate sym x  = liftIO (W4.realNeg (w4 sym) x)
+  realMinus sym x y = liftIO (W4.realSub (w4 sym) x y)
+  realMult sym x y  = liftIO (W4.realMul (w4 sym) x y)
+  realRecip sym x   =
+    do one <- liftIO (W4.realLit (w4 sym) 1)
+       realDiv sym one x
+  realDiv sym x y =
+    do assertRealDivisor sym y
+       liftIO (W4.realDiv (w4 sym) x y)
+
+  realEq sym x y          = liftIO (W4.realEq (w4 sym) x y)
+  realLessThan sym x y    = liftIO (W4.realLt (w4 sym) x y)
+  realGreaterThan sym x y = liftIO (W4.realGt (w4 sym) x y)
+
+  realFloor sym x       = liftIO (W4.realFloor (w4 sym) x)
+  realCeiling sym x     = liftIO (W4.realCeil (w4 sym) x)
+  realTrunc sym x       = liftIO (W4.realTrunc (w4 sym) x)
+  realRoundAway sym x   = liftIO (W4.realRound (w4 sym) x)
+  realRoundToEven sym x = liftIO (W4.realRoundEven (w4 sym) x)
+
   -- NB, we don't do reduction here on symbolic values
   intToZn sym m x
     | Just xi <- W4.asInteger x
diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs
index 67718a09c..c66bc7f77 100644
--- a/src/Cryptol/Eval.hs
+++ b/src/Cryptol/Eval.hs
@@ -443,6 +443,7 @@ etaDelay sym env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
       VWord{}     -> x
       VRational{} -> x
       VFloat{}    -> x
+      VReal{}     -> x
       VSeq n xs ->
         case tp of
           TVSeq _nt el -> return $ VSeq n $ IndexSeqMap $ \i -> go stk el (lookupSeqMap xs i)
@@ -484,6 +485,7 @@ etaDelay sym env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
     case tp of
       TVBit -> v
       TVInteger -> v
+      TVReal -> v
       TVFloat {} -> v
       TVIntMod _ -> v
       TVRational -> v
diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs
index 28c7c0e9f..26530c5c4 100644
--- a/src/Cryptol/Eval/Concrete.hs
+++ b/src/Cryptol/Eval/Concrete.hs
@@ -94,6 +94,9 @@ toExpr prims t0 v0 = findOne (go t0 v0)
         do let n' = ETApp (ETApp (prim "number") (tNum n)) tInteger
            let d' = ETApp (ETApp (prim "number") (tNum d)) tInteger
            pure $ EApp (EApp (prim "ratio") n') d'
+      VReal r ->
+        do q <- go tRational (VRational (SRational (numerator r) (denominator r)))
+           pure $ EApp (prim "fromRational") q
       VFloat i ->
         do (eT, pT) <- maybe mismatch pure (tIsFloat ty)
            pure (floatToExpr prims eT pT (bfValue i))
@@ -118,6 +121,7 @@ toExpr prims t0 v0 = findOne (go t0 v0)
              , render doc
              ]
 
+
 floatToExpr :: PrimMap -> AST.Type -> AST.Type -> FP.BigFloat -> AST.Expr
 floatToExpr prims eT pT f =
   case FP.bfToRep f of
diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index 750ef4643..48fb4dbd0 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -64,6 +64,7 @@ mkLit sym ty i =
     TVFloat e p                  -> VFloat <$> fpLit sym e p (fromInteger i)
     TVSeq w TVBit                -> pure $ word sym w i
     TVRational                   -> VRational <$> (intToRational sym =<< integerLit sym i)
+    TVReal                       -> VReal <$> realLit sym (fromInteger i :: Rational)
     _                            -> evalPanic "Cryptol.Eval.Prim.evalConst"
                                     [ "Invalid type for number" ]
 
@@ -94,6 +95,7 @@ intV sym i =
     (pure i)
     (\m -> intToZn sym m i)
     (intToRational sym i)
+    (intToReal sym i)
     (\e p -> fpRndMode sym >>= \r -> fpFromInteger sym e p r i)
 
 {-# SPECIALIZE ratioV :: Concrete -> Prim Concrete #-}
@@ -117,6 +119,7 @@ ecFractionV sym =
   PPrim
     case ty of
       TVFloat e p -> VFloat <$> fpLit sym e p (n % d)
+      TVReal -> VReal <$> realLit sym (n % d)
       TVRational ->
         do x <- integerLit sym n
            y <- integerLit sym d
@@ -166,6 +169,7 @@ type BinWord sym = Integer -> SWord sym -> SWord sym -> SEval sym (SWord sym)
       (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
       (Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
       (SRational Concrete -> SRational Concrete -> SEval Concrete (SRational Concrete)) ->
+      (SReal Concrete -> SReal Concrete -> SEval Concrete (SReal Concrete)) ->
       (SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->
       Binary Concrete
   #-}
@@ -177,9 +181,10 @@ ringBinary :: forall sym.
   (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
   (Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
   (SRational sym -> SRational sym -> SEval sym (SRational sym)) ->
+  (SReal sym -> SReal sym -> SEval sym (SReal sym)) ->
   (SFloat sym -> SFloat sym -> SEval sym (SFloat sym)) ->
   Binary sym
-ringBinary sym opw opi opz opq opfp = loop
+ringBinary sym opw opi opz opq opr opfp = loop
   where
   loop' :: TValue
         -> SEval sym (GenValue sym)
@@ -207,6 +212,9 @@ ringBinary sym opw opi opz opq opfp = loop
     TVRational ->
       VRational <$> opq (fromVRational l) (fromVRational r)
 
+    TVReal ->
+      VReal <$> opr (fromVReal l) (fromVReal r)
+
     TVArray{} ->
       evalPanic "arithBinary" ["Array not in class Ring"]
 
@@ -256,6 +264,7 @@ type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym)
   (SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
   (Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
   (SRational Concrete -> SEval Concrete (SRational Concrete)) ->
+  (SReal Concrete -> SEval Concrete (SReal Concrete)) ->
   (SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->
   Unary Concrete
   #-}
@@ -266,9 +275,10 @@ ringUnary :: forall sym.
   (SInteger sym -> SEval sym (SInteger sym)) ->
   (Integer -> SInteger sym -> SEval sym (SInteger sym)) ->
   (SRational sym -> SEval sym (SRational sym)) ->
+  (SReal sym -> SEval sym (SReal sym)) ->
   (SFloat sym -> SEval sym (SFloat sym)) ->
   Unary sym
-ringUnary sym opw opi opz opq opfp = loop
+ringUnary sym opw opi opz opq opr opfp = loop
   where
   loop' :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
   loop' ty v = loop ty =<< v
@@ -291,6 +301,9 @@ ringUnary sym opw opi opz opq opfp = loop
     TVRational ->
       VRational <$> opq (fromVRational v)
 
+    TVReal ->
+      VReal <$> opr (fromVReal v)
+
     TVArray{} ->
       evalPanic "arithUnary" ["Array not in class Ring"]
 
@@ -329,6 +342,7 @@ ringUnary sym opw opi opz opq opfp = loop
   SEval Concrete (SInteger Concrete) ->
   (Integer -> SEval Concrete (SInteger Concrete)) ->
   SEval Concrete (SRational Concrete) ->
+  SEval Concrete (SReal Concrete) ->
   (Integer -> Integer -> SEval Concrete (SFloat Concrete)) ->
   TValue ->
   SEval Concrete (GenValue Concrete)
@@ -341,10 +355,11 @@ ringNullary :: forall sym.
   SEval sym (SInteger sym) ->
   (Integer -> SEval sym (SInteger sym)) ->
   SEval sym (SRational sym) ->
+  SEval sym (SReal sym) ->
   (Integer -> Integer -> SEval sym (SFloat sym)) ->
   TValue ->
   SEval sym (GenValue sym)
-ringNullary sym opw opi opz opq opfp = loop
+ringNullary sym opw opi opz opq opr opfp = loop
   where
     loop :: TValue -> SEval sym (GenValue sym)
     loop ty =
@@ -359,6 +374,8 @@ ringNullary sym opw opi opz opq opfp = loop
 
         TVRational -> VRational <$> opq
 
+        TVReal -> VReal <$> opr 
+
         TVArray{} -> evalPanic "arithNullary" ["Array not in class Ring"]
 
         TVSeq w a
@@ -431,42 +448,46 @@ fromIntegerV sym =
 
 {-# INLINE addV #-}
 addV :: Backend sym => sym -> Binary sym
-addV sym = ringBinary sym opw opi opz opq opfp
+addV sym = ringBinary sym opw opi opz opq opr opfp
   where
     opw _w x y = wordPlus sym x y
     opi x y = intPlus sym x y
     opz m x y = znPlus sym m x y
     opq x y = rationalAdd sym x y
+    opr x y = realPlus sym x y
     opfp x y = fpRndMode sym >>= \r -> fpPlus sym r x y
 
 {-# INLINE subV #-}
 subV :: Backend sym => sym -> Binary sym
-subV sym = ringBinary sym opw opi opz opq opfp
+subV sym = ringBinary sym opw opi opz opq opr opfp
   where
     opw _w x y = wordMinus sym x y
     opi x y = intMinus sym x y
     opz m x y = znMinus sym m x y
     opq x y = rationalSub sym x y
+    opr x y = realMinus sym x y
     opfp x y = fpRndMode sym >>= \r -> fpMinus sym r x y
 
 {-# INLINE negateV #-}
 negateV :: Backend sym => sym -> Unary sym
-negateV sym = ringUnary sym opw opi opz opq opfp
+negateV sym = ringUnary sym opw opi opz opq opr opfp
   where
     opw _w x = wordNegate sym x
     opi x = intNegate sym x
     opz m x = znNegate sym m x
     opq x = rationalNegate sym x
+    opr x = realNegate sym x
     opfp x = fpNeg sym x
 
 {-# INLINE mulV #-}
 mulV :: Backend sym => sym -> Binary sym
-mulV sym = ringBinary sym opw opi opz opq opfp
+mulV sym = ringBinary sym opw opi opz opq opr opfp
   where
     opw _w x y = wordMult sym x y
     opi x y = intMult sym x y
     opz m x y = znMult sym m x y
     opq x y = rationalMul sym x y
+    opr x y = realMult sym x y
     opfp x y = fpRndMode sym >>= \r -> fpMult sym r x y
 
 --------------------------------------------------
@@ -568,6 +589,7 @@ recipV sym =
   PPrim
     case a of
       TVRational -> VRational <$> (rationalRecip sym . fromVRational =<< x)
+      TVReal -> VReal <$> (realRecip sym . fromVReal =<< x)
       TVFloat e p ->
         do one <- fpLit sym e p 1
            r   <- fpRndMode sym
@@ -588,6 +610,10 @@ fieldDivideV sym =
         do x' <- fromVRational <$> x
            y' <- fromVRational <$> y
            VRational <$> rationalDivide sym x' y'
+      TVReal ->
+        do x' <- fromVReal <$> x
+           y' <- fromVReal <$> y
+           VReal <$> realDiv sym x' y'
       TVFloat _e _p ->
         do xv <- fromVFloat <$> x
            yv <- fromVFloat <$> y
@@ -608,6 +634,7 @@ fieldDivideV sym =
   Concrete ->
   String ->
   (SRational Concrete -> SEval Concrete (SInteger Concrete)) ->
+  (SReal Concrete -> SEval Concrete (SInteger Concrete)) ->
   (SFloat Concrete -> SEval Concrete (SInteger Concrete)) ->
   Unary Concrete #-}
 
@@ -616,47 +643,54 @@ roundOp ::
   sym ->
   String ->
   (SRational sym -> SEval sym (SInteger sym)) ->
+  (SReal sym -> SEval sym (SInteger sym)) ->
   (SFloat sym -> SEval sym (SInteger sym)) ->
   Unary sym
-roundOp _sym nm qop opfp ty v =
+roundOp _sym nm qop rop opfp ty v =
   case ty of
-    TVRational  -> VInteger <$> (qop (fromVRational v))
+    TVRational  -> VInteger <$> qop (fromVRational v)
+    TVReal      -> VInteger <$> rop (fromVReal v)
     TVFloat _ _ -> VInteger <$> opfp (fromVFloat v)
     _ -> evalPanic nm [show ty ++ " is not a Field"]
 
 {-# INLINE floorV #-}
 floorV :: Backend sym => sym -> Unary sym
-floorV sym = roundOp sym "floor" opq opfp
+floorV sym = roundOp sym "floor" opq opr opfp
   where
   opq = rationalFloor sym
+  opr = realFloor sym
   opfp = \x -> fpRndRTN sym >>= \r -> fpToInteger sym "floor" r x
 
 {-# INLINE ceilingV #-}
 ceilingV :: Backend sym => sym -> Unary sym
-ceilingV sym = roundOp sym "ceiling" opq opfp
+ceilingV sym = roundOp sym "ceiling" opq opr opfp
   where
   opq = rationalCeiling sym
+  opr = realCeiling sym
   opfp = \x -> fpRndRTP sym >>= \r -> fpToInteger sym "ceiling" r x
 
 {-# INLINE truncV #-}
 truncV :: Backend sym => sym -> Unary sym
-truncV sym = roundOp sym "trunc" opq opfp
+truncV sym = roundOp sym "trunc" opq opr opfp
   where
   opq = rationalTrunc sym
+  opr = realTrunc sym
   opfp = \x -> fpRndRTZ sym >>= \r -> fpToInteger sym "trunc" r x
 
 {-# INLINE roundAwayV #-}
 roundAwayV :: Backend sym => sym -> Unary sym
-roundAwayV sym = roundOp sym "roundAway" opq opfp
+roundAwayV sym = roundOp sym "roundAway" opq opr opfp
   where
   opq = rationalRoundAway sym
+  opr = realRoundAway sym
   opfp = \x -> fpRndRNA sym >>= \r -> fpToInteger sym "roundAway" r x
 
 {-# INLINE roundToEvenV #-}
 roundToEvenV :: Backend sym => sym -> Unary sym
-roundToEvenV sym = roundOp sym "roundToEven" opq opfp
+roundToEvenV sym = roundOp sym "roundToEven" opq opr opfp
   where
   opq = rationalRoundToEven sym
+  opr = realRoundToEven sym
   opfp = \x -> fpRndRNE sym >>= \r -> fpToInteger sym "roundToEven" r x
 
 --------------------------------------------------------------
@@ -712,6 +746,7 @@ smodV sym  =
   (SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (SRational Concrete -> SRational Concrete -> SEval Concrete a -> SEval Concrete a) ->
+  (SReal Concrete -> SReal Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (SFloat Concrete -> SFloat Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (TValue -> GenValue Concrete -> GenValue Concrete -> SEval Concrete a -> SEval Concrete a)
   #-}
@@ -724,9 +759,10 @@ cmpValue ::
   (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
   (Integer -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
   (SRational sym -> SRational sym -> SEval sym a -> SEval sym a) ->
+  (SReal sym -> SReal sym -> SEval sym a -> SEval sym a) ->
   (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a) ->
   (TValue -> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a)
-cmpValue sym fb fw fi fz fq ff = cmp
+cmpValue sym fb fw fi fz fq fr ff = cmp
   where
     cmp ty v1 v2 k =
       case ty of
@@ -735,6 +771,7 @@ cmpValue sym fb fw fi fz fq ff = cmp
         TVFloat _ _   -> ff (fromVFloat v1) (fromVFloat v2) k
         TVIntMod n    -> fz n (fromVInteger v1) (fromVInteger v2) k
         TVRational    -> fq (fromVRational v1) (fromVRational v2) k
+        TVReal        -> fr (fromVReal v1) (fromVReal v2) k
         TVArray{}     -> panic "Cryptol.Prims.Value.cmpValue"
                                [ "Arrays are not comparable" ]
         TVSeq n t
@@ -777,37 +814,40 @@ bitGreaterThan sym x y = bitLessThan sym y x
 
 {-# INLINE valEq #-}
 valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
-valEq sym ty v1 v2 = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym True)
+valEq sym ty v1 v2 = cmpValue sym fb fw fi fz fq fr ff ty v1 v2 (pure $ bitLit sym True)
   where
   fb x y k   = eqCombine sym (bitEq  sym x y) k
   fw x y k   = eqCombine sym (wordEq sym x y) k
   fi x y k   = eqCombine sym (intEq  sym x y) k
   fz m x y k = eqCombine sym (znEq sym m x y) k
   fq x y k   = eqCombine sym (rationalEq sym x y) k
+  fr x y k   = eqCombine sym (realEq sym x y) k
   ff x y k   = eqCombine sym (fpEq sym x y) k
 
 {-# INLINE valLt #-}
 valLt :: Backend sym =>
   sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
-valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)
+valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq fr ff ty v1 v2 (pure final)
   where
   fb x y k   = lexCombine sym (bitLessThan  sym x y) (bitEq  sym x y) k
   fw x y k   = lexCombine sym (wordLessThan sym x y) (wordEq sym x y) k
   fi x y k   = lexCombine sym (intLessThan  sym x y) (intEq  sym x y) k
   fz _ _ _ _ = panic "valLt" ["Z_n is not in `Cmp`"]
   fq x y k   = lexCombine sym (rationalLessThan sym x y) (rationalEq sym x y) k
+  fr x y k   = lexCombine sym (realLessThan sym x y) (realEq sym x y) k
   ff x y k   = lexCombine sym (fpLessThan   sym x y) (fpEq   sym x y) k
 
 {-# INLINE valGt #-}
 valGt :: Backend sym =>
   sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
-valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)
+valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq fr ff ty v1 v2 (pure final)
   where
   fb x y k   = lexCombine sym (bitGreaterThan  sym x y) (bitEq  sym x y) k
   fw x y k   = lexCombine sym (wordGreaterThan sym x y) (wordEq sym x y) k
   fi x y k   = lexCombine sym (intGreaterThan  sym x y) (intEq  sym x y) k
   fz _ _ _ _ = panic "valGt" ["Z_n is not in `Cmp`"]
   fq x y k   = lexCombine sym (rationalGreaterThan sym x y) (rationalEq sym x y) k
+  fr x y k   = lexCombine sym (realGreaterThan sym x y) (realEq sym x y) k
   ff x y k   = lexCombine sym (fpGreaterThan   sym x y) (fpEq   sym x y) k
 
 {-# INLINE eqCombine #-}
@@ -856,13 +896,14 @@ greaterThanEqV sym ty v1 v2 = VBit <$> valGt sym ty v1 v2 (bitLit sym True)
 
 {-# INLINE signedLessThanV #-}
 signedLessThanV :: Backend sym => sym -> Binary sym
-signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym False)
+signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz fq fr ff ty v1 v2 (pure $ bitLit sym False)
   where
   fb _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on bit type"]
   fw x y k   = lexCombine sym (wordSignedLessThan sym x y) (wordEq sym x y) k
   fi _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Integer type"]
   fz m _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on Z_" ++ show m ++ " type"]
   fq _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Rational type"]
+  fr _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Real type"]
   ff _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Float"]
 
 
@@ -894,6 +935,9 @@ zeroV sym ty = case ty of
   TVRational ->
     VRational <$> (intToRational sym =<< integerLit sym 0)
 
+  TVReal ->
+    VReal <$> realLit sym 0
+
   TVArray{} -> evalPanic "zeroV" ["Array not in class Zero"]
 
   -- floating point
@@ -1304,6 +1348,7 @@ logicBinary sym opb opw = loop
     TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]
     TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"]
     TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
+    TVReal     -> evalPanic "logicBinary" ["Real not in class Logic"]
     TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"]
 
     TVFloat {}  -> evalPanic "logicBinary" ["Float not in class Logic"]
@@ -1382,6 +1427,7 @@ logicUnary sym opb opw = loop
     TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"]
     TVFloat {} -> evalPanic "logicUnary" ["Float not in class Logic"]
     TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
+    TVReal     -> evalPanic "logicBinary" ["Real not in class Logic"]
     TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"]
 
     TVSeq w ety
@@ -1837,6 +1883,7 @@ errorV sym ty0 msg =
        TVInteger -> err stk
        TVIntMod _ -> err stk
        TVRational -> err stk
+       TVReal -> err stk
        TVArray{} -> err stk
        TVFloat {} -> err stk
 
@@ -1938,6 +1985,7 @@ mergeValue sym c v1 v2 =
     (VBit b1     , VBit b2     ) -> VBit <$> iteBit sym c b1 b2
     (VInteger i1 , VInteger i2 ) -> VInteger <$> iteInteger sym c i1 i2
     (VRational q1, VRational q2) -> VRational <$> iteRational sym c q1 q2
+    (VReal r1    , VReal r2)     -> VReal <$> iteReal sym c r1 r2
     (VWord n1 w1 , VWord n2 w2 ) | n1 == n2 -> pure $ VWord n1 $ mergeWord' sym c w1 w2
     (VSeq n1 vs1 , VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 <$> memoMap sym (mergeSeqMap sym c vs1 vs2)
     (VStream vs1 , VStream vs2 ) -> VStream <$> memoMap sym (mergeSeqMap sym c vs1 vs2)
diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs
index ad6300f4c..7941260dd 100644
--- a/src/Cryptol/Eval/Reference.lhs
+++ b/src/Cryptol/Eval/Reference.lhs
@@ -78,6 +78,7 @@ are as follows:
 | `Integer`         | integers          | `TVInteger`                 |
 | `Z n`             | integers modulo n | `TVIntMod n`                |
 | `Rational`        | rationals         | `TVRational`                |
+| `Real`            | real numbers      | `TVReal`
 | `Float e p`       | floating point    | `TVFloat`                   |
 | `Array`           | arrays            | `TVArray`                   |
 | `[n]a`            | finite lists      | `TVSeq n a`                 |
@@ -167,6 +168,7 @@ terms by providing an evaluator to an appropriate `Value` type.
 >   = VBit !Bool                 -- ^ @ Bit    @ booleans
 >   | VInteger !Integer          -- ^ @ Integer @  or @Z n@ integers
 >   | VRational !Rational        -- ^ @ Rational @ rationals
+>   | VReal !Rational            -- ^ @ Real @ real numbers
 >   | VFloat !BF                 -- ^ Floating point numbers
 >   | VList Nat' [E Value]       -- ^ @ [n]a   @ finite or infinite lists
 >   | VTuple [E Value]           -- ^ @ ( .. ) @ tuples
@@ -193,6 +195,11 @@ Operations on Values
 > fromVRational (VRational i) = i
 > fromVRational _             = evalPanic "fromVRational" ["Expected a rational"]
 >
+> -- | Destructor for @VReal@.
+> fromVReal :: Value -> Rational
+> fromVReal (VReal i) = i
+> fromVReal _         = evalPanic "fromVReal" ["Expected a real"]
+>
 > fromVFloat :: Value -> BigFloat
 > fromVFloat = bfValue . fromVFloat'
 >
@@ -902,6 +909,7 @@ For functions, `zero` returns the constant function that returns
 > zero TVInteger      = VInteger 0
 > zero TVIntMod{}     = VInteger 0
 > zero TVRational     = VRational 0
+> zero TVReal         = VReal 0
 > zero (TVFloat e p)  = VFloat (fpToBF e p FP.bfPosZero)
 > zero TVArray{}      = evalPanic "zero" ["Array type not in `Zero`"]
 > zero (TVSeq n ety)  = VList (Nat n) (genericReplicate n (pure (zero ety)))
@@ -978,6 +986,7 @@ at the same positions.
 >         TVIntMod _   -> evalPanic "logicUnary" ["Z not in class Logic"]
 >         TVArray{}    -> evalPanic "logicUnary" ["Array not in class Logic"]
 >         TVRational   -> evalPanic "logicUnary" ["Rational not in class Logic"]
+>         TVReal       -> evalPanic "logicUnary" ["Real not in class Logic"]
 >         TVFloat{}    -> evalPanic "logicUnary" ["Float not in class Logic"]
 >         TVAbstract{} -> evalPanic "logicUnary" ["Abstract type not in `Logic`"]
 
@@ -1016,6 +1025,7 @@ at the same positions.
 >         TVIntMod _   -> evalPanic "logicBinary" ["Z not in class Logic"]
 >         TVArray{}    -> evalPanic "logicBinary" ["Array not in class Logic"]
 >         TVRational   -> evalPanic "logicBinary" ["Rational not in class Logic"]
+>         TVReal       -> evalPanic "logicBinary" ["Real not in class Logic"]
 >         TVFloat{}    -> evalPanic "logicBinary" ["Float not in class Logic"]
 >         TVAbstract{} -> evalPanic "logicBinary" ["Abstract type not in `Logic`"]
 
@@ -1048,6 +1058,8 @@ False]`, but to `error "foo"`.
 >           VInteger . flip mod n <$> i
 >         TVRational ->
 >           VRational <$> q
+>         TVReal ->
+>           VReal <$> q
 >         TVFloat e p ->
 >           VFloat . fpToBF e p <$> fl e p
 >         TVArray{} ->
@@ -1086,6 +1098,8 @@ False]`, but to `error "foo"`.
 >           VInteger <$> appOp1 (\i -> flip mod n <$> iop i) (fromVInteger <$> val)
 >         TVRational ->
 >           VRational <$> appOp1 qop (fromVRational <$> val)
+>         TVReal ->
+>           VReal <$> appOp1 qop (fromVReal <$> val)
 >         TVFloat e p ->
 >           VFloat . fpToBF e p <$> appOp1 (flop e p) (fromVFloat <$> val)
 >         TVSeq w a
@@ -1122,6 +1136,8 @@ False]`, but to `error "foo"`.
 >           VInteger <$> appOp2 (\i j -> flip mod n <$> iop i j) (fromVInteger <$> l) (fromVInteger <$> r)
 >         TVRational ->
 >           VRational <$> appOp2 qop (fromVRational <$> l) (fromVRational <$> r)
+>         TVReal ->
+>           VReal <$> appOp2 qop (fromVReal <$> l) (fromVReal <$> r)
 >         TVFloat e p ->
 >           VFloat . fpToBF e p <$>
 >             appOp2 (flop e p) (fromVFloat <$> l) (fromVFloat <$> r)
@@ -1212,6 +1228,7 @@ confused with integral division).
 >               TValue -> E Value -> E Value
 > fieldUnary qop zop flop ty v = case ty of
 >   TVRational  -> VRational <$> appOp1 qop (fromVRational <$> v)
+>   TVReal      -> VReal <$> appOp1 qop (fromVReal <$> v)
 >   TVIntMod m  -> VInteger <$> appOp1 (zop m) (fromVInteger <$> v)
 >   TVFloat e p -> VFloat . fpToBF e p <$> appOp1 (flop e p) (fromVFloat <$> v)
 >   _ -> evalPanic "fieldUnary" [show ty ++ " is not a Field type"]
@@ -1224,6 +1241,8 @@ confused with integral division).
 > fieldBinary qop zop flop ty l r = case ty of
 >   TVRational  -> VRational <$>
 >                    appOp2 qop (fromVRational <$> l) (fromVRational <$> r)
+>   TVReal      -> VReal <$>
+>                    appOp2 qop (fromVReal <$> l) (fromVReal <$> r)
 >   TVIntMod m  -> VInteger <$>
 >                    appOp2 (zop m) (fromVInteger <$> l) (fromVInteger <$> r)
 >   TVFloat e p -> VFloat . fpToBF e p <$>
@@ -1254,6 +1273,7 @@ Round
 >               TValue -> E Value -> E Value
 > roundUnary op flop ty v = case ty of
 >   TVRational -> VInteger . op . fromVRational <$> v
+>   TVReal     -> VInteger . op . fromVReal <$> v
 >   TVFloat {} -> VInteger <$> (flop . fromVFloat' =<< v)
 >   _ -> evalPanic "roundUnary" [show ty ++ " is not a Round type"]
 >
@@ -1306,6 +1326,8 @@ bits to the *left* of that position are equal.
 >       compare <$> (fromVInteger <$> l) <*> (fromVInteger <$> r)
 >     TVRational ->
 >       compare <$> (fromVRational <$> l) <*> (fromVRational <$> r)
+>     TVReal ->
+>       compare <$> (fromVReal <$> l) <*> (fromVReal <$> r)
 >     TVFloat{} ->
 >       compare <$> (fromVFloat <$> l) <*> (fromVFloat <$> r)
 >     TVArray{} ->
@@ -1357,6 +1379,8 @@ fields are compared in alphabetical order.
 >       evalPanic "lexSignedCompare" ["invalid type"]
 >     TVRational ->
 >       evalPanic "lexSignedCompare" ["invalid type"]
+>     TVReal ->
+>       evalPanic "lexSignedCompare" ["invalid type"]
 >     TVFloat{} ->
 >       evalPanic "lexSignedCompare" ["invalid type"]
 >     TVArray{} ->
@@ -1664,6 +1688,7 @@ Pretty Printing
 >     VBit b     -> text (show b)
 >     VInteger i -> text (show i)
 >     VRational q -> text (show q)
+>     VReal q -> text (show q)
 >     VFloat fl -> text (show (FP.fpPP opts fl))
 >     VList l vs ->
 >       case l of
diff --git a/src/Cryptol/Eval/Type.hs b/src/Cryptol/Eval/Type.hs
index 49fad0521..b5ab0128c 100644
--- a/src/Cryptol/Eval/Type.hs
+++ b/src/Cryptol/Eval/Type.hs
@@ -32,6 +32,7 @@ data TValue
   | TVFloat Integer Integer   -- ^ @ Float e p @
   | TVIntMod Integer          -- ^ @ Z n @
   | TVRational                -- ^ @Rational@
+  | TVReal                    -- ^ @Real@
   | TVArray TValue TValue     -- ^ @ Array a b @
   | TVSeq Integer TValue      -- ^ @ [n]a @
   | TVStream TValue           -- ^ @ [inf]t @
@@ -50,6 +51,7 @@ tValTy tv =
     TVFloat e p -> tFloat (tNum e) (tNum p)
     TVIntMod n  -> tIntMod (tNum n)
     TVRational  -> tRational
+    TVReal      -> tReal
     TVArray a b -> tArray (tValTy a) (tValTy b)
     TVSeq n t   -> tSeq (tNum n) (tValTy t)
     TVStream t  -> tSeq tInf (tValTy t)
@@ -109,6 +111,7 @@ evalType env ty =
         (TCBit, [])     -> Right $ TVBit
         (TCInteger, []) -> Right $ TVInteger
         (TCRational, []) -> Right $ TVRational
+        (TCReal, [])    -> Right $ TVReal
         (TCFloat, [e,p])-> Right $ TVFloat (inum e) (inum p)
         (TCIntMod, [n]) -> case num n of
                              Inf   -> evalPanic "evalType" ["invalid type Z inf"]
diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs
index a488034d5..bb0cb667a 100644
--- a/src/Cryptol/Eval/Value.hs
+++ b/src/Cryptol/Eval/Value.hs
@@ -45,6 +45,7 @@ module Cryptol.Eval.Value
   , fromVBit
   , fromVInteger
   , fromVRational
+  , fromVReal
   , fromVFloat
   , fromVSeq
   , fromSeq
@@ -95,6 +96,7 @@ import Data.Bits
 import Data.IORef
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
+import Data.Ratio
 import MonadLib
 
 import Cryptol.Backend
@@ -309,6 +311,7 @@ data GenValue sym
   | VBit !(SBit sym)                           -- ^ @ Bit    @
   | VInteger !(SInteger sym)                   -- ^ @ Integer @ or @ Z n @
   | VRational !(SRational sym)                 -- ^ @ Rational @
+  | VReal !(SReal sym)                         -- ^ @ Real @
   | VFloat !(SFloat sym)
   | VSeq !Integer !(SeqMap sym)                -- ^ @ [n]a   @
                                                --   Invariant: VSeq is never a sequence of bits
@@ -334,6 +337,7 @@ forceValue v = case v of
   VBit b      -> seq b (return ())
   VInteger i  -> seq i (return ())
   VRational q -> seq q (return ())
+  VReal r     -> seq r (return ())
   VFloat f    -> seq f (return ())
   VWord _ wv  -> forceWordValue =<< wv
   VStream _   -> return ()
@@ -350,6 +354,7 @@ instance Backend sym => Show (GenValue sym) where
     VBit _     -> "bit"
     VInteger _ -> "integer"
     VRational _ -> "rational"
+    VReal _    -> "real"
     VFloat _   -> "float"
     VSeq n _   -> "seq:" ++ show n
     VWord n _  -> "word:"  ++ show n
@@ -380,6 +385,14 @@ ppValue x opts = loop
     VBit b             -> return $ ppBit x b
     VInteger i         -> return $ ppInteger x opts i
     VRational q        -> return $ ppRational x opts q
+    VReal r
+      | Just q <- realAsLit x r ->
+          do n <- integerLit x (numerator q)
+             d <- integerLit x (denominator q)
+             let ppq = ppRational x opts (SRational n d)
+             pure (parens (text "fromRational" <+> ppq)) 
+      | otherwise -> return $ text "[?]"
+
     VFloat i           -> return $ ppFloat x opts i
     VSeq sz vals       -> ppWordSeq sz vals
     VWord _ wv         -> ppWordVal =<< wv
@@ -495,6 +508,11 @@ fromVRational val = case val of
   VRational q -> q
   _      -> evalPanic "fromVRational" ["not a Rational"]
 
+fromVReal :: GenValue sym -> SReal sym
+fromVReal val = case val of
+  VReal r -> r
+  _       -> evalPanic "fromVReal" ["not a Real"]
+
 -- | Extract a finite sequence value.
 fromVSeq :: GenValue sym -> SeqMap sym
 fromVSeq val = case val of
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
index 02a6afd43..3cb67e9c8 100644
--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@@ -140,6 +140,7 @@ data FinType
     | FTInteger
     | FTIntMod Integer
     | FTRational
+    | FTReal
     | FTFloat Integer Integer
     | FTSeq Int FinType
     | FTTuple [FinType]
@@ -157,6 +158,7 @@ finType ty =
     TVInteger        -> Just FTInteger
     TVIntMod n       -> Just (FTIntMod n)
     TVRational       -> Just FTRational
+    TVReal           -> Just FTReal
     TVFloat e p      -> Just (FTFloat e p)
     TVSeq n t        -> FTSeq <$> numType n <*> finType t
     TVTuple ts       -> FTTuple <$> traverse finType ts
@@ -171,6 +173,7 @@ unFinType fty =
     FTInteger    -> tInteger
     FTIntMod n   -> tIntMod (tNum n)
     FTRational   -> tRational
+    FTReal       -> tReal
     FTFloat e p  -> tFloat (tNum e) (tNum p)
     FTSeq l ety  -> tSeq (tNum l) (unFinType ety)
     FTTuple ftys -> tTuple (unFinType <$> ftys)
@@ -181,6 +184,7 @@ data VarShape sym
   = VarBit (SBit sym)
   | VarInteger (SInteger sym)
   | VarRational (SInteger sym) (SInteger sym)
+  | VarReal (SReal sym)
   | VarFloat (SFloat sym)
   | VarWord (SWord sym)
   | VarFinSeq Integer [VarShape sym]
@@ -193,6 +197,7 @@ ppVarShape sym (VarInteger i) = ppInteger sym defaultPPOpts i
 ppVarShape sym (VarFloat f) = ppFloat sym defaultPPOpts f
 ppVarShape sym (VarRational n d) =
   text "(ratio" <+> ppInteger sym defaultPPOpts n <+> ppInteger sym defaultPPOpts d <+> text ")"
+ppVarShape _sym (VarReal _) = text "<<real>>"
 ppVarShape sym (VarWord w) = ppWord sym defaultPPOpts w
 ppVarShape sym (VarFinSeq _ xs) =
   brackets (fsep (punctuate comma (map (ppVarShape sym) xs)))
@@ -210,6 +215,7 @@ varShapeToValue sym var =
     VarBit b     -> VBit b
     VarInteger i -> VInteger i
     VarRational n d -> VRational (SRational n d)
+    VarReal r    -> VReal r
     VarWord w    -> VWord (wordLen sym w) (return (WordVal w))
     VarFloat f   -> VFloat f
     VarFinSeq n vs -> VSeq n (finiteSeqMap (map (pure . varShapeToValue sym) vs))
@@ -221,6 +227,7 @@ data FreshVarFns sym =
   { freshBitVar     :: IO (SBit sym)
   , freshWordVar    :: Integer -> IO (SWord sym)
   , freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger sym)
+  , freshRealVar    :: IO (SReal sym)
   , freshFloatVar   :: Integer -> Integer -> IO (SFloat sym)
   }
 
@@ -231,6 +238,7 @@ freshVar fns tp = case tp of
     FTRational    -> VarRational
                         <$> freshIntegerVar fns Nothing Nothing
                         <*> freshIntegerVar fns (Just 1) Nothing
+    FTReal        -> VarReal <$> freshRealVar fns
     FTIntMod 0    -> panic "freshVariable" ["0 modulus not allowed"]
     FTIntMod m    -> VarInteger  <$> freshIntegerVar fns (Just 0) (Just (m-1))
     FTFloat e p   -> VarFloat    <$> freshFloatVar fns e p
@@ -283,6 +291,9 @@ varModelPred sym vx =
          d' <- integerLit sym dlit
          rationalEq sym (SRational n d) (SRational n' d')
 
+    (VarReal r, VarReal rlit) ->
+      realEq sym r =<< realLit sym rlit
+
     (VarWord w, VarWord (Concrete.BV len wlit)) ->
       wordEq sym w =<< wordLit sym len wlit
 
@@ -328,6 +339,13 @@ varToExpr prims = go
             d' = ETApp (ETApp (prim "number") (tNum d)) tInteger
          in EApp (EApp (prim "ratio") n') d'
 
+      (FTReal, VarReal r) ->
+        EProofApp $ ePrim prims (prelPrim "fraction")
+                          `ETApp` tNum (numerator r)
+                          `ETApp` tNum (denominator r)
+                          `ETApp` tNum (0 :: Int)
+                          `ETApp` tReal
+
       (FTFloat e p, VarFloat f) ->
         floatToExpr prims e p (bfValue f)
 
diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs
index 168a4c216..413d4eda6 100644
--- a/src/Cryptol/Symbolic/SBV.hs
+++ b/src/Cryptol/Symbolic/SBV.hs
@@ -492,6 +492,10 @@ parseValue FTInteger cvs =
     Just (x, cvs') -> (VarInteger x, cvs')
     Nothing        -> panic "Cryptol.Symbolic.parseValue" [ "no integer" ]
 parseValue (FTIntMod _) cvs = parseValue FTInteger cvs
+parseValue FTReal cvs =
+  case cvs of
+    (SBV.CV SBV.KReal cv : cvs') -> error "parseValue SBV Real!"
+    _ -> panic "Cryptol.Symbolic.parseValue" [ "no real" ]
 parseValue FTRational cvs =
   fromMaybe (panic "Cryptol.Symbolic.parseValue" ["no rational"]) $
   do (n,cvs')  <- SBV.genParse SBV.KUnbounded cvs
@@ -539,5 +543,6 @@ sbvFreshFns sym =
   { freshBitVar     = freshSBool_ sym
   , freshWordVar    = freshBV_ sym . fromInteger
   , freshIntegerVar = freshBoundedInt sym
+  , freshRealVar    = freshSReal_ sym
   , freshFloatVar   = \_ _ -> return () -- TODO
   }
diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs
index b53a8af46..22314b0b6 100644
--- a/src/Cryptol/Symbolic/What4.hs
+++ b/src/Cryptol/Symbolic/What4.hs
@@ -223,6 +223,7 @@ what4FreshFns sym =
   { freshBitVar     = W4.freshConstant sym W4.emptySymbol W4.BaseBoolRepr
   , freshWordVar    = SW.freshBV sym W4.emptySymbol
   , freshIntegerVar = W4.freshBoundedInt sym W4.emptySymbol
+  , freshRealVar    = W4.freshConstant sym W4.emptySymbol W4.BaseRealRepr
   , freshFloatVar   = W4.fpFresh sym
   }
 
@@ -544,6 +545,7 @@ varShapeToConcrete evalFn v =
     VarBit b -> VarBit <$> W4.groundEval evalFn b
     VarInteger i -> VarInteger <$> W4.groundEval evalFn i
     VarRational n d -> VarRational <$> W4.groundEval evalFn n <*> W4.groundEval evalFn d
+    VarReal r -> VarReal <$> W4.groundEval evalFn r
     VarWord SW.ZBV -> pure (VarWord (Concrete.mkBv 0 0))
     VarWord (SW.DBV x) ->
       let w = W4.intValue (W4.bvWidth x)
diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs
index 9b5a2926e..442a69769 100644
--- a/src/Cryptol/Testing/Random.hs
+++ b/src/Cryptol/Testing/Random.hs
@@ -134,6 +134,7 @@ randomValue sym ty =
     TVBit         -> Just (randomBit sym)
     TVInteger     -> Just (randomInteger sym)
     TVRational    -> Just (randomRational sym)
+    TVReal        -> Just (randomReal sym)
     TVIntMod m    -> Just (randomIntMod sym m)
     TVFloat e p   -> Just (randomFloat sym e p)
     TVSeq n TVBit -> Just (randomWord sym n)
@@ -200,6 +201,9 @@ randomRational sym w g =
           pure (VRational (SRational n' d'))
        , g3)
 
+randomReal :: (Backend sym, RandomGen g) => sym -> Gen g sym
+randomReal = error "TODO randomReal"
+
 {-# INLINE randomWord #-}
 
 -- | Generate a random word of the given length (i.e., a value of type @[w]@)
@@ -351,6 +355,7 @@ typeSize ty = case ty of
   TVBit -> Just 2
   TVInteger -> Nothing
   TVRational -> Nothing
+  TVReal -> Nothing
   TVIntMod n -> Just n
   TVFloat{} -> Nothing -- TODO?
   TVArray{} -> Nothing
@@ -369,6 +374,7 @@ typeValues ty =
     TVBit      -> [ VBit False, VBit True ]
     TVInteger  -> []
     TVRational -> []
+    TVReal     -> []
     TVIntMod n -> [ VInteger x | x <- [ 0 .. (n-1) ] ]
     TVFloat{}  -> [] -- TODO?
     TVArray{}  -> []
diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs
index 87bd879eb..38d5e9e7c 100644
--- a/src/Cryptol/TypeCheck/Solver/Class.hs
+++ b/src/Cryptol/TypeCheck/Solver/Class.hs
@@ -79,11 +79,12 @@ solveZeroInst ty = case tNoUser ty of
   -- Zero (Z n)
   TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne ]
 
-  -- Zero Real
-
   -- Zero Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Zero Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- ValidVloat e p => Zero (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
@@ -120,6 +121,9 @@ solveLogicInst ty = case tNoUser ty of
   -- Logic Rational fails
   TCon (TC TCRational) [] -> Unsolvable
 
+  -- Logic Real fails
+  TCon (TC TCReal) [] -> Unsolvable
+
   -- Logic (Float e p) fails
   TCon (TC TCFloat) [_, _] -> Unsolvable
 
@@ -166,6 +170,9 @@ solveRingInst ty = case tNoUser ty of
   -- Ring Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Ring Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- ValidFloat e p => Ring (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
@@ -236,6 +243,9 @@ solveFieldInst ty = case tNoUser ty of
   -- Field Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Field Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- ValidFloat e p => Field (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
@@ -278,6 +288,9 @@ solveRoundInst ty = case tNoUser ty of
   -- Round Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Round Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- ValidFloat e p => Round (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
@@ -315,6 +328,9 @@ solveEqInst ty = case tNoUser ty of
   -- Eq Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Eq Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- ValidFloat e p => Eq (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
@@ -352,6 +368,9 @@ solveCmpInst ty = case tNoUser ty of
   -- Cmp Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Cmp Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- Cmp (Z n) fails
   TCon (TC TCIntMod) [_] -> Unsolvable
 
@@ -407,6 +426,9 @@ solveSignedCmpInst ty = case tNoUser ty of
   -- SignedCmp Rational fails
   TCon (TC TCRational) [] -> Unsolvable
 
+  -- SignedCmp Real fails
+  TCon (TC TCReal) [] -> Unsolvable
+
   -- SignedCmp (Float e p) fails
   TCon (TC TCFloat) [_, _] -> Unsolvable
 
@@ -442,6 +464,9 @@ solveFLiteralInst numT denT rndT ty
       TCon (TC TCRational) [] ->
         SolvedIf [ pFin numT, pFin denT, denT >== tOne ]
 
+      TCon (TC TCReal) [] ->
+        SolvedIf [ pFin numT, pFin denT, denT >== tOne ]
+
       TCon (TC TCFloat) [e,p]
         | Just 0    <- tIsNum rndT ->
           SolvedIf [ pValidFloat e p
@@ -478,6 +503,9 @@ solveLiteralInst val ty
       -- (fin val) => Literal val Rational
       TCon (TC TCRational) [] -> SolvedIf [ pFin val ]
 
+      -- (fin val) => Literal val Real
+      TCon (TC TCReal) [] -> SolvedIf [ pFin val ]
+
       -- ValidFloat e p => Literal val (Float e p)   if `val` is representable
       TCon (TC TCFloat) [e,p]
         | Just n    <- tIsNum val
diff --git a/src/Cryptol/TypeCheck/TCon.hs b/src/Cryptol/TypeCheck/TCon.hs
index 654286036..8582c2ffe 100644
--- a/src/Cryptol/TypeCheck/TCon.hs
+++ b/src/Cryptol/TypeCheck/TCon.hs
@@ -62,6 +62,7 @@ builtInType nm =
     , "Bit"               ~> TC TCBit
     , "Integer"           ~> TC TCInteger
     , "Rational"          ~> TC TCRational
+    , "Real"              ~> TC TCReal
     , "Z"                 ~> TC TCIntMod
 
       -- Predicate contstructors
@@ -136,6 +137,7 @@ instance HasKind TC where
       TCBit     -> KType
       TCInteger -> KType
       TCRational -> KType
+      TCReal    -> KType
       TCFloat   -> KNum :-> KNum :-> KType
       TCIntMod  -> KNum :-> KType
       TCArray   -> KType :-> KType :-> KType
@@ -232,6 +234,7 @@ data TC     = TCNum Integer            -- ^ Numbers
             | TCFloat                  -- ^ Float
             | TCIntMod                 -- ^ @Z _@
             | TCRational               -- ^ @Rational@
+            | TCReal                   -- ^ @Real@
             | TCArray                  -- ^ @Array _ _@
             | TCSeq                    -- ^ @[_] _@
             | TCFun                    -- ^ @_ -> _@
@@ -330,6 +333,7 @@ instance PP TC where
       TCInteger -> text "Integer"
       TCIntMod  -> text "Z"
       TCRational -> text "Rational"
+      TCReal    -> text "Real"
       TCArray   -> text "Array"
       TCFloat   -> text "Float"
       TCSeq     -> text "[]"
diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs
index 4c664f226..8890fecd6 100644
--- a/src/Cryptol/TypeCheck/Type.hs
+++ b/src/Cryptol/TypeCheck/Type.hs
@@ -439,6 +439,12 @@ tIsRational ty =
     TCon (TC TCRational) [] -> True
     _                       -> False
 
+tIsReal :: Type -> Bool
+tIsReal ty =
+  case tNoUser ty of
+    TCon (TC TCReal) [] -> True
+    _                   -> False
+
 tIsFloat :: Type -> Maybe (Type, Type)
 tIsFloat ty =
   case tNoUser ty of
@@ -593,6 +599,9 @@ tInteger  = TCon (TC TCInteger) []
 tRational :: Type
 tRational  = TCon (TC TCRational) []
 
+tReal :: Type
+tReal = TCon (TC TCReal) []
+
 tFloat   :: Type -> Type -> Type
 tFloat e p = TCon (TC TCFloat) [ e, p ]
 
@@ -939,6 +948,7 @@ instance PP (WithNames Type) where
           (TCBit,   [])       -> text "Bit"
           (TCInteger, [])     -> text "Integer"
           (TCRational, [])    -> text "Rational"
+          (TCReal, [])        -> text "Real"
 
           (TCIntMod, [n])     -> optParens (prec > 3) $ text "Z" <+> go 5 n