diff options
author | Son Ho | 2023-12-05 17:34:13 +0100 |
---|---|---|
committer | Son Ho | 2023-12-05 17:34:13 +0100 |
commit | 726db4911add81a853aafcec3936b457aaeff5b4 (patch) | |
tree | 2663915767c3558203990ed14f8d5604b7fd21d1 /tests/fstar/misc/PoloniusList.fst | |
parent | 92887b89e35607e99bae2f19e4c5b2f162683d02 (diff) | |
parent | 4795e5f823bc89504855d8eb946b111d9314f4d5 (diff) |
Merge branch 'main' into son_fixes2
Diffstat (limited to 'tests/fstar/misc/PoloniusList.fst')
-rw-r--r-- | tests/fstar/misc/PoloniusList.fst | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst index 79c86606..188b22d8 100644 --- a/tests/fstar/misc/PoloniusList.fst +++ b/tests/fstar/misc/PoloniusList.fst @@ -5,27 +5,30 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [polonius_list::List] *) +(** [polonius_list::List] + Source: 'src/polonius_list.rs', lines 3:0-3:16 *) type list_t (t : Type0) = -| ListCons : t -> list_t t -> list_t t -| ListNil : list_t t +| List_Cons : t -> list_t t -> list_t t +| List_Nil : list_t t -(** [polonius_list::get_list_at_x]: forward function *) -let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) = +(** [polonius_list::get_list_at_x]: forward function + Source: 'src/polonius_list.rs', lines 13:0-13:76 *) +let rec get_list_at_x (ls : list_t u32) (x : u32) : result (list_t u32) = begin match ls with - | ListCons hd tl -> - if hd = x then Return (ListCons hd tl) else get_list_at_x_fwd tl x - | ListNil -> Return ListNil + | List_Cons hd tl -> + if hd = x then Return (List_Cons hd tl) else get_list_at_x tl x + | List_Nil -> Return List_Nil end -(** [polonius_list::get_list_at_x]: backward function 0 *) +(** [polonius_list::get_list_at_x]: backward function 0 + Source: 'src/polonius_list.rs', lines 13:0-13:76 *) 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 - | ListCons hd tl -> + | List_Cons hd tl -> if hd = x then Return ret - else let* tl0 = get_list_at_x_back tl x ret in Return (ListCons hd tl0) - | ListNil -> Return ret + else let* tl0 = get_list_at_x_back tl x ret in Return (List_Cons hd tl0) + | List_Nil -> Return ret end |