summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2022-10-13 18:04:31 +0200
committerSon Ho2022-10-13 18:04:31 +0200
commite7b4aba11391bede785799237a73ef7bd16d0372 (patch)
treec114050af416caef7c539cfb7ae10df889540ae6 /tests
parente692a9535cecc8a19fea9d0ebf2b470a09cf4541 (diff)
Use "polonius" in the names instead of "nll"
Diffstat (limited to 'tests')
-rw-r--r--tests/misc/BetreePolonius.fst (renamed from tests/misc/BetreeNll.fst)10
1 files changed, 5 insertions, 5 deletions
diff --git a/tests/misc/BetreeNll.fst b/tests/misc/BetreePolonius.fst
index b548a18b..2bac07b6 100644
--- a/tests/misc/BetreeNll.fst
+++ b/tests/misc/BetreePolonius.fst
@@ -1,16 +1,16 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_nll] *)
-module BetreeNll
+(** [betree_polonius] *)
+module BetreePolonius
open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [betree_nll::List] *)
+(** [betree_polonius::List] *)
type list_t (t : Type0) =
| ListCons : t -> list_t t -> list_t t
| ListNil : list_t t
-(** [betree_nll::get_list_at_x] *)
+(** [betree_polonius::get_list_at_x] *)
let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
begin match ls with
| ListCons hd tl ->
@@ -24,7 +24,7 @@ let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
| ListNil -> Return ListNil
end
-(** [betree_nll::get_list_at_x] *)
+(** [betree_polonius::get_list_at_x] *)
let rec get_list_at_x_back
(ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) =
begin match ls with