summaryrefslogtreecommitdiff
path: root/fstar
diff options
context:
space:
mode:
authorSon Ho2022-02-03 23:18:00 +0100
committerSon Ho2022-02-03 23:18:00 +0100
commitf7f5d626745200df5748e7bda860c7d303bea18a (patch)
tree1865b1e72ee781134f39401204422756ad883513 /fstar
parent72edb3fc4fdfa588d0cebe7fec27101da27ff1be (diff)
Make mor modifications
Diffstat (limited to '')
-rw-r--r--fstar/Primitives.fst3
1 files changed, 3 insertions, 0 deletions
diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst
index 6771fe93..b8da70c4 100644
--- a/fstar/Primitives.fst
+++ b/fstar/Primitives.fst
@@ -9,6 +9,9 @@ type result (a : Type0) : Type0 =
| Return : a -> result a
| Fail : result a
+(*** Misc *)
+type char = FStar.Char.char
+
(*** Scalars *)
/// Rk.: most of the following code was at least partially generated
let isize_min : int = -9223372036854775808