From 304490110509324a20c7c2c3be9bf61931fa3a1c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 17 Dec 2022 10:50:43 +0100
Subject: Make minor modifications and generate code for loops

---
 tests/fstar/misc/Loops.Clauses.Template.fst | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 tests/fstar/misc/Loops.Clauses.Template.fst

(limited to 'tests/fstar/misc/Loops.Clauses.Template.fst')

diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
new file mode 100644
index 00000000..a898e9fb
--- /dev/null
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -0,0 +1,13 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [loops]: templates for the decreases clauses *)
+module Loops.Clauses.Template
+open Primitives
+open Loops.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [loops::list_nth_mut_loop]: decreases clause *)
+unfold
+let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
+  admit ()
+
-- 
cgit v1.2.3