Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Commit

Permalink
updated Prelude.hs to use new, simpler defineModuleFromFileWithFns fu…
Browse files Browse the repository at this point in the history
…nction
  • Loading branch information
Eddy Westbrook committed May 10, 2018
1 parent 7832110 commit 3668afa
Showing 1 changed file with 2 additions and 6 deletions.
8 changes: 2 additions & 6 deletions src/Verifier/SAW/Prelude.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,9 @@ import Verifier.SAW.ParserUtils
import Verifier.SAW.Prelude.Constants
import Verifier.SAW.SharedTerm

$(runDecWriter $ do
prelude <- defineModuleFromFile [] "preludeModule" "prelude/Prelude.sawcore"
declareSharedModuleFns "Prelude" (decVal prelude)
)
$(defineModuleFromFileWithFns "preludeModule" "prelude/Prelude.sawcore")

scEq :: SharedContext -> Term -> Term -> IO Term
scEq sc x y = do
xty <- scTypeOf sc x
eqOp <- scApplyPrelude_eq sc
eqOp xty x y
scApplyPrelude_eq sc xty x y

0 comments on commit 3668afa

Please sign in to comment.