From e2f714d8a415dd5ec7c3e5bf0fa6b3511f4f925a Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 22 Oct 2020 05:41:25 -0700
Subject: [PATCH] Add function `scToIntMod` to SharedTerm library.

---
 saw-core/src/Verifier/SAW/SharedTerm.hs | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
index 7d6ab1f8..b8b0ae12 100644
--- a/saw-core/src/Verifier/SAW/SharedTerm.hs
+++ b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -172,6 +172,7 @@ module Verifier.SAW.SharedTerm
   , scIntToBv, scBvToInt, scSbvToInt
     -- *** IntMod
   , scIntModType
+  , scToIntMod
     -- *** Vectors
   , scAppend
   , scJoin
@@ -1709,6 +1710,12 @@ scSbvToInt sc n x = scGlobalApply sc "Prelude.sbvToInt" [n,x]
 scIntModType :: SharedContext -> Term -> IO Term
 scIntModType sc n = scGlobalApply sc "Prelude.IntMod" [n]
 
+-- | Convert an integer to an integer mod n.
+--
+-- > toIntMod : (n : Nat) -> Integer -> IntMod n;
+scToIntMod :: SharedContext -> Term -> Term -> IO Term
+scToIntMod sc n x = scGlobalApply sc "Prelude.toIntMod" [n, x]
+
 
 -- Primitive operations on bitvectors