diff options
Diffstat (limited to 'tests/fstar/misc/Matches.fst')
| -rw-r--r-- | tests/fstar/misc/Matches.fst | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/tests/fstar/misc/Matches.fst b/tests/fstar/misc/Matches.fst new file mode 100644 index 00000000..06a9b6df --- /dev/null +++ b/tests/fstar/misc/Matches.fst @@ -0,0 +1,12 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [matches] *) +module Matches +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [matches::match_u32]: + Source: 'tests/src/matches.rs', lines 4:0-4:27 *) +let match_u32 (x : u32) : result u32 = + begin match x with | 0 -> Ok 0 | 1 -> Ok 1 | _ -> Ok 2 end + |