blob: 1fd3e6b023ee466a869eaa94d9b8a1c81cfc42f2 (
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 16)))
(def: #export I16
(:by_example [size]
(Sub size)
..sub
(I64 size)))
(def: #export equivalence (Equivalence I16) (\ ..sub &equivalence))
(def: #export width Nat (\ ..sub width))
(def: #export i16 (-> I64 I16) (\ ..sub narrow))
(def: #export i64 (-> I16 I64) (\ ..sub widen))
|