Add some tests

1 files changed, 54 insertions, 0 deletions

diff --git a/tests/coq/misc/Issue194RecursiveStructProjector.v b/tests/coq/misc/Issue194RecursiveStructProjector.v
new file mode 100644
index 00000000..d1a07449
--- /dev/null
+++ b/tests/coq/misc/Issue194RecursiveStructProjector.v
@@ -0,0 +1,54 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [issue_194_recursive_struct_projector] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module Issue194RecursiveStructProjector.
+
+(** [issue_194_recursive_struct_projector::AVLNode]
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-2:17 *)
+Inductive AVLNode_t (T : Type) :=
+| mkAVLNode_t :
+  T ->
+  option (AVLNode_t T) ->
+  option (AVLNode_t T) ->
+  AVLNode_t T
+.
+
+Arguments mkAVLNode_t { _ }.
+
+Definition aVLNode_value {T : Type} (x : AVLNode_t T) :=
+  match x with | mkAVLNode_t x1 _ _ => x1 end
+.
+
+Notation "x2 .(aVLNode_value)" := (aVLNode_value x2) (at level 9).
+
+Definition aVLNode_left {T : Type} (x : AVLNode_t T) :=
+  match x with | mkAVLNode_t _ x1 _ => x1 end
+.
+
+Notation "x2 .(aVLNode_left)" := (aVLNode_left x2) (at level 9).
+
+Definition aVLNode_right {T : Type} (x : AVLNode_t T) :=
+  match x with | mkAVLNode_t _ _ x1 => x1 end
+.
+
+Notation "x2 .(aVLNode_right)" := (aVLNode_right x2) (at level 9).
+
+(** [issue_194_recursive_struct_projector::get_val]:
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 10:0-10:33 *)
+Definition get_val (T : Type) (x : AVLNode_t T) : result T :=
+  Ok x.(aVLNode_value)
+.
+
+(** [issue_194_recursive_struct_projector::get_left]:
+    Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 14:0-14:43 *)
+Definition get_left
+  (T : Type) (x : AVLNode_t T) : result (option (AVLNode_t T)) :=
+  Ok x.(aVLNode_left)
+.
+
+End Issue194RecursiveStructProjector.