Add a test for issue 270

tests/coq/misc/Issue270LoopList.v

@@ -0,0 +1,33 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [issue_270_loop_list] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module Issue270LoopList.
+
+(** [issue_270_loop_list::List]
+    Source: 'tests/src/issue-270-loop-list.rs', lines 2:0-5:1 *)
+Inductive List_t (T : Type) :=
+| List_Cons : T -> List_t T -> List_t T
+| List_Nil : List_t T
+.
+
+Arguments List_Cons { _ }.
+Arguments List_Nil { _ }.
+
+(** [issue_270_loop_list::foo]: loop 0:
+    Source: 'tests/src/issue-270-loop-list.rs', lines 11:8-14:9 *)
+Fixpoint foo_loop (t : List_t (List_t u8)) : result unit :=
+  match t with | List_Cons _ tt1 => foo_loop tt1 | List_Nil => Ok tt end
+.
+
+(** [issue_270_loop_list::foo]:
+    Source: 'tests/src/issue-270-loop-list.rs', lines 8:0-16:1 *)
+Definition foo (v : List_t (List_t u8)) : result unit :=
+  match v with | List_Cons l t => foo_loop t | List_Nil => Ok tt end
+.
+
+End Issue270LoopList.

tests/fstar/misc/Issue270LoopList.fst

@@ -0,0 +1,23 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [issue_270_loop_list] *)
+module Issue270LoopList
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [issue_270_loop_list::List]
+    Source: 'tests/src/issue-270-loop-list.rs', lines 2:0-5:1 *)
+type list_t (t : Type0) =
+| List_Cons : t -> list_t t -> list_t t
+| List_Nil : list_t t
+
+(** [issue_270_loop_list::foo]: loop 0:
+    Source: 'tests/src/issue-270-loop-list.rs', lines 11:8-14:9 *)
+let rec foo_loop (t : list_t (list_t u8)) : result unit =
+  begin match t with | List_Cons _ tt -> foo_loop tt | List_Nil -> Ok () end
+
+(** [issue_270_loop_list::foo]:
+    Source: 'tests/src/issue-270-loop-list.rs', lines 8:0-16:1 *)
+let foo (v : list_t (list_t u8)) : result unit =
+  begin match v with | List_Cons l t -> foo_loop t | List_Nil -> Ok () end
+

tests/lean/Issue270LoopList.lean

@@ -0,0 +1,31 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [issue_270_loop_list]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace issue_270_loop_list
+
+/- [issue_270_loop_list::List]
+   Source: 'tests/src/issue-270-loop-list.rs', lines 2:0-5:1 -/
+inductive List (T : Type) :=
+| Cons : T → List T → List T
+| Nil : List T
+
+/- [issue_270_loop_list::foo]: loop 0:
+   Source: 'tests/src/issue-270-loop-list.rs', lines 11:8-14:9 -/
+divergent def foo_loop (t : List (List U8)) : Result Unit :=
+  match t with
+  | List.Cons _ tt => foo_loop tt
+  | List.Nil => Result.ok ()
+
+/- [issue_270_loop_list::foo]:
+   Source: 'tests/src/issue-270-loop-list.rs', lines 8:0-16:1 -/
+def foo (v : List (List U8)) : Result Unit :=
+  match v with
+  | List.Cons l t => foo_loop t
+  | List.Nil => Result.ok ()
+
+end issue_270_loop_list

tests/src/issue-270-loop-list.rs

@@ -0,0 +1,16 @@
+//@ [coq,fstar] subdir=misc
+pub enum List<T> {
+    Cons(T, Box<List<T>>),
+    Nil,
+}
+
+
+fn foo(v: &List<List<u8>>) {
+    if let List::Cons(_, t) = v {
+        let mut t = &**t;
+        while let List::Cons(_, tt) = t
+        {
+            t = &**tt;
+        }
+    }
+}