(** 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.