blob: e9dfbd0621b3e799917207ddd497793b4de30ddc (
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
33
34
35
36
37
|
==================== Tidy Core ====================
Result size of Tidy Core
= {terms: 36, types: 100, coercions: 56, joins: 0/0}
nat2Word#
= \ @n $dKnownNat _ ->
naturalToWord# ($dKnownNat `cast` <Co:5> :: KnownNat n ~R# Natural)
foo = \ _ -> 18##
fd
= \ @n $dKnownNat _ ->
naturalToWord#
($dKnownNat
`cast` <Co:13> :: KnownNat (Div (n + 63) 64) ~R# Natural)
d = \ _ -> 3##
fm
= \ @n $dKnownNat _ ->
naturalToWord#
($dKnownNat
`cast` <Co:17> :: KnownNat (Mod (n - 1) 64 + 1) ~R# Natural)
m = \ _ -> 9##
fp
= \ @n $dKnownNat _ ->
naturalToWord#
($dKnownNat
`cast` <Co:21> :: KnownNat (2 ^ (Mod (n + 63) 64 + 1)) ~R# Natural)
p = \ _ -> 512##
|
