blob: 16da5b679fa8f5e011c2592f934e7b558346dedd (
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
|
(.module:
[library
[lux (#- i64)
[abstract
[equivalence (#+ Equivalence)]]
[data
["." maybe]]
[type (#+ :by_example)]]]
[//
["." i64 (#+ Sub)]])
(def: sub
(maybe.assume (i64.sub 8)))
(def: #export I8
(:by_example [size]
(Sub size)
..sub
(I64 size)))
(def: #export equivalence (Equivalence I8) (\ ..sub &equivalence))
(def: #export width Nat (\ ..sub width))
(def: #export i8 (-> I64 I8) (\ ..sub narrow))
(def: #export i64 (-> I8 I64) (\ ..sub widen))
|
