(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [loops] *)
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
Local Open Scope Primitives_scope.
Module Loops.

(** [loops::List] *)
Inductive List_t (T : Type) :=
| ListCons : T -> List_t T -> List_t T
| ListNil : List_t T
.

Arguments ListCons {T} _ _.
Arguments ListNil {T}.

(** [loops::list_nth_mut_loop] *)
Fixpoint list_nth_mut_loop_loop0_fwd
  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match ls with
    | ListCons x tl =>
      if i s= 0%u32
      then Return x
      else (
        i0 <- u32_sub i 1%u32;
        t <- list_nth_mut_loop_loop0_fwd T n0 tl i0;
        Return t)
    | ListNil => Fail_ Failure
    end
  end
.

(** [loops::list_nth_mut_loop] *)
Definition list_nth_mut_loop_fwd
  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
  t <- list_nth_mut_loop_loop0_fwd T n ls i; Return t
.

(** [loops::list_nth_mut_loop] *)
Fixpoint list_nth_mut_loop_loop0_back
  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
  result (List_t T)
  :=
  match n with
  | O => Fail_ OutOfFuel
  | S n0 =>
    match ls with
    | ListCons x tl =>
      if i s= 0%u32
      then Return (ListCons ret tl)
      else (
        i0 <- u32_sub i 1%u32;
        l <- list_nth_mut_loop_loop0_back T n0 tl i0 ret;
        Return (ListCons x l))
    | ListNil => Fail_ Failure
    end
  end
.

(** [loops::list_nth_mut_loop] *)
Definition list_nth_mut_loop_back
  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) :
  result (List_t T)
  :=
  l <- list_nth_mut_loop_loop0_back T n ls i ret; Return l
.

End Loops .