We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 34c54ee commit 1579247Copy full SHA for 1579247
1 file changed
README.md
@@ -1 +1,32 @@
1
-# binary
+# binary
2
+Lean 4 package for binary data serialization and deserialization, with name `binary` inspired by Haskell's `binary` package.
3
+
4
+# Usage
5
+Add to `lakefile.lean`:
6
+```
7
+require binary from git "https://github.com/Qiu233/binary"
8
9
10
+In file:
11
12
13
+import Binary
14
15
+open Binary Primitive.LE
16
+...
17
18
19
+Or open `Primitive.BE` when you want to handle data in big endian.
20
21
+The recommended usage is
22
23
24
25
26
+open Binary Primitive
27
28
+open LE in
29
+def serialize_xxx : Put := do
30
+ ...
31
32
0 commit comments