blob: 9959bae6d370cf9b22f28703a463110f9da8d20e (
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 (.except i64)
[type (.only by_example)]
[abstract
[equivalence (.only Equivalence)]]
[control
["[0]" maybe]]]]
[//
["[0]" i64 (.only 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))
|
