Fix some tests.

FStarLang · Jan 16, 2025 · 1a7e6bc · 1a7e6bc
1 parent 3c95da7
commit 1a7e6bc
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 5 deletions.
diff --git a/doc/book/code/Pure.fst b/doc/book/code/Pure.fst
@@ -15,7 +15,7 @@ let fact (x:nat) : pos = factorial x
 
 //SNIPPET_START: wp$
 let pre = Type0
-let post (a:Type) = a -> Type0
+let post (a:Type) = a -> GTot Type0
 let wp (a:Type) = post a -> pre
 //SNIPPET_END: wp$
 

diff --git a/doc/old/tutorial/code/exercises/Ex04e.fst b/doc/old/tutorial/code/exercises/Ex04e.fst
@@ -20,6 +20,7 @@ type option 'a =
    | None : option 'a
    | Some : v:'a -> option 'a
 
+val find : f:('a -> Tot bool) -> list 'a -> Tot (option (x:'a{f x}))
 let rec find f l = match l with
   | [] -> None
   | hd::tl -> if f hd then Some hd else find f tl

diff --git a/examples/algorithms/GC.fst b/examples/algorithms/GC.fst
@@ -83,7 +83,7 @@ type mutator_inv gc_state =
   inv gc_state (fun i -> gc_state.color i = Unalloc \/ gc_state.color i = White)
 
 new_effect GC_STATE = STATE_h gc_state
-let gc_post (a:Type) = a -> gc_state -> Type0
+let gc_post (a:Type) = a -> gc_state -> GTot Type0
 sub_effect
   DIV   ~> GC_STATE = fun (a:Type) (wp:pure_wp a) (p:gc_post a) (gc:gc_state) -> wp (fun a -> p a gc)
 

diff --git a/examples/algorithms/IntervalIntersect.fst b/examples/algorithms/IntervalIntersect.fst
@@ -589,7 +589,7 @@ let rec ppIntervals' (is:intervals): ML unit =
 
 let toI f t = I (int_to_t f) (int_to_t t)
 
-let ppIntervals is : ML string = FStar.List.Tot.fold_left (sprintf "%s %s") "" (FStar.List.map ppInterval is)
+let ppIntervals is : ML string = FStar.List.Tot.fold_left (sprintf "%s %s") "" (FStar.List.map (fun i -> ppInterval i) is)
 let main =
   print_string
     (ppIntervals (intersect [toI 3 10; toI 10 15] [toI 1 4; toI 10 14]));

diff --git a/examples/doublylinkedlist/DoublyLinkedList.fst b/examples/doublylinkedlist/DoublyLinkedList.fst
@@ -1101,8 +1101,8 @@ let tot_dll_to_fragment_split (#t:Type) (h0:heap) (d:dll t{dll_valid h0 d})
           reveal d.nodes == reveal p1.pnodes `append` reveal p2.pnodes))) =
   let split_nodes = elift2_p split_using d.nodes (hide n2) in
   lemma_split_using d.nodes n2;
-  let l1 = elift1 fst split_nodes in
-  let l2 = elift1 snd split_nodes in
+  let l1 = hide (fst split_nodes) in
+  let l2 = hide (snd split_nodes) in
   let p1 = { phead = d.lhead ; ptail = n1 ; pnodes = l1 } in
   let p2 = { phead = n2 ; ptail = d.ltail ; pnodes = l2 } in
   let f = Frag2 p1 p2 in