diff options
| author | Nadrieril | 2024-05-27 17:33:56 +0200 |
|---|---|---|
| committer | Nadrieril | 2024-05-28 11:36:31 +0200 |
| commit | c81c96f20b1dbf428a9ed42e83b910e798e1a225 (patch) | |
| tree | b01e01eb4bcec7112399647943047bed3b58cad1 /tests/fstar/misc/Matches.fst | |
| parent | 9cc69020773cc77965a6faa6f0d46f179de3d8b8 (diff) | |
Add some tests
Diffstat (limited to '')
| -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 + |