From c81c96f20b1dbf428a9ed42e83b910e798e1a225 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 17:33:56 +0200
Subject: Add some tests

---
 tests/fstar/misc/Matches.fst | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 tests/fstar/misc/Matches.fst

(limited to 'tests/fstar/misc/Matches.fst')

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
+
-- 
cgit v1.2.3