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

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

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

diff --git a/tests/fstar/misc/Issue194RecursiveStructProjector.fst b/tests/fstar/misc/Issue194RecursiveStructProjector.fst
new file mode 100644
index 00000000..76368f04
--- /dev/null
+++ b/tests/fstar/misc/Issue194RecursiveStructProjector.fst
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [issue_194_recursive_struct_projector] *)
+module Issue194RecursiveStructProjector
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [issue_194_recursive_struct_projector::AVLNode]
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-2:17 *)
+type aVLNode_t (t : Type0) =
+{
+  value : t; left : option (aVLNode_t t); right : option (aVLNode_t t);
+}
+
+(** [issue_194_recursive_struct_projector::get_val]:
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 10:0-10:33 *)
+let get_val (t : Type0) (x : aVLNode_t t) : result t =
+  Ok x.value
+
+(** [issue_194_recursive_struct_projector::get_left]:
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 14:0-14:43 *)
+let get_left (t : Type0) (x : aVLNode_t t) : result (option (aVLNode_t t)) =
+  Ok x.left
+
-- 
cgit v1.2.3