Skip to content

Commit cfd99bd

Browse files
authored
Merge pull request #2575 from ucsd-progsys/define-Integer-IS
Add assumption and define for GHC.Num.Integer.IS
2 parents f049893 + f5bdd64 commit cfd99bd

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/GHC/Num/Integer_LHAssumptions.hs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,5 +10,7 @@ import GHC.Types_LHAssumptions()
1010
{-@
1111
assume GHC.Num.Integer.IS :: x:Int# -> {v: Integer | v = (x :: int) }
1212

13+
define GHC.Num.Integer.IS x = (x)
14+
1315
embed Integer as int
1416
@-}

0 commit comments

Comments
 (0)