blob: 942c1f222a5cf9cadc6c6ccf6dcd5e6d1a4adcf4 (
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
|
(.using
[library
[lux {"-" i64}
[type {"+" by_example}]
[abstract
[equivalence {"+" Equivalence}]]
[control
["[0]" maybe]]]]
[//
["[0]" i64 {"+" Sub}]])
(def: sub
(maybe.trusted (i64.sub 8)))
(def: .public I8
Type
... TODO: Switch to the cleaner approach ASAP.
(case (type_of ..sub)
{.#Apply :size: :sub:}
(type (I64 :size:))
_
(undefined))
... (by_example [size]
... (Sub size)
... ..sub
... (I64 size))
)
(def: .public equivalence (Equivalence I8) (# ..sub sub_equivalence))
(def: .public width Nat (# ..sub bits))
(def: .public i8 (-> I64 I8) (# ..sub narrow))
(def: .public i64 (-> I8 I64) (# ..sub wide))
|