diff options
author | Son Ho | 2022-02-03 23:18:00 +0100 |
---|---|---|
committer | Son Ho | 2022-02-03 23:18:00 +0100 |
commit | f7f5d626745200df5748e7bda860c7d303bea18a (patch) | |
tree | 1865b1e72ee781134f39401204422756ad883513 /fstar | |
parent | 72edb3fc4fdfa588d0cebe7fec27101da27ff1be (diff) |
Make mor modifications
Diffstat (limited to '')
-rw-r--r-- | fstar/Primitives.fst | 3 |
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 |