We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 26cae83 commit 9d6af78Copy full SHA for 9d6af78
1 file changed
README.md
@@ -7,9 +7,30 @@ Add to `lakefile.lean`:
7
require binary from git "https://github.com/Lean-zh/binary.git"
8
```
9
10
-In file:
+## Deriving
11
+```lean
12
+import Binary
13
+
14
+open Binary Primitive
15
16
+open LE in
17
+@[bin_enum 4 [0, 2]]
18
+inductive A where
19
+ | a -- 0
20
+ | b (s : Int32) -- 2
21
+deriving Encode, Decode
22
23
+open BE in
24
+structure B where
25
+ s : Int32
26
27
28
+#eval Put.run 128 (put (A.b 1234))
29
30
31
+## Serialization/Deserialization
32
33
34
import Binary
35
36
open Binary Primitive.LE
@@ -20,7 +41,7 @@ Or open `Primitive.BE` when you want to handle data in big endian.
41
42
The recommended usage is
43
-```
44
45
46
47
open Binary Primitive
0 commit comments