From 1a7e6bc63ec14a160569d0fbf1af4f72dd7f9153 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 15 Jan 2025 11:15:25 -0800
Subject: [PATCH] Fix some tests.

---
 doc/book/code/Pure.fst                         | 2 +-
 doc/old/tutorial/code/exercises/Ex04e.fst      | 1 +
 examples/algorithms/GC.fst                     | 2 +-
 examples/algorithms/IntervalIntersect.fst      | 2 +-
 examples/doublylinkedlist/DoublyLinkedList.fst | 4 ++--
 5 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/doc/book/code/Pure.fst b/doc/book/code/Pure.fst
index f051aabc2f6..e3411785027 100644
--- 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
index dbdc9b6bb21..9927872093a 100644
--- 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
index bc76739edb3..837585e4053 100644
--- 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
index 32d31578a8d..70e524abc3a 100644
--- 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
index d529f88e79f..9c3967e149b 100644
--- 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