blob: 8f6e3696bede3b80f57da5dbe06f9c0486ec3515 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
==================== Tidy Core ====================
Result size of Tidy Core
= {terms: 22, types: 20, coercions: 0, joins: 0/0}
integer_to_int
= \ x ->
case x of {
IS ipv -> Just (I# ipv);
IP x1 -> Nothing;
IN ds -> Nothing
}
natural_to_word
= \ x ->
case x of {
NS x1 -> Just (W# x1);
NB ds -> Nothing
}
------ Local rules for imported ids --------
"SPEC/Test toIntegralSized @Natural @Word"
forall $dIntegral $dIntegral1 $dBits $dBits1.
toIntegralSized $dIntegral $dIntegral1 $dBits $dBits1
= natural_to_word
"SPEC/Test toIntegralSized @Integer @Int"
forall $dIntegral $dIntegral1 $dBits $dBits1.
toIntegralSized $dIntegral $dIntegral1 $dBits $dBits1
= integer_to_int
|
