summaryrefslogtreecommitdiff
path: root/fstar
diff options
context:
space:
mode:
Diffstat (limited to 'fstar')
-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