val is_list (#t: _) (x: llist t) (l: list t) : Tot vprop (decreases l)
val is_list (#t: _) (x: llist t) (l: list t) : Tot vprop (decreases l)
let rec is_list #t (x:llist t) (l:list t)
: Tot vprop (decreases l)
= match l with
  | [] -> pure (x == None)
  | head::tl -> 
    exists* (p:node_ptr t) (tail:llist t).
      pure (x == Some p) **
      pts_to p { head; tail } **
      is_list tail tl
module PulseTutorial.LinkedList
open Pulse.Lib.Pervasives
module S = Pulse.Lib.Stick.Util
module FA = Pulse.Lib.Forall.Util
open FStar.List.Tot

//llist$
noeq
type node (t:Type0) = {
    head : t;
    tail : llist t;
}

and node_ptr (t:Type0) = ref (node t)

//A nullable pointer to a node
and llist (t:Type0) = option (node_ptr t)
//llist$
/
Pulse.Lib.Stick.Util.fst.checked Pulse.Lib.Pervasives.fst.checked Pulse.Lib.Forall.Util.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
PulseTutorial.LinkedList.fst
x: PulseTutorial.LinkedList.llist t -> l: Prims.list t -> Prims.Tot Pulse.Lib.Core.vprop
PulseTutorial.LinkedList.llist Prims.list Pulse.Lib.Core.pure Prims.eq2 FStar.Pervasives.Native.option Pulse.Lib.Reference.ref PulseTutorial.LinkedList.node FStar.Pervasives.Native.None Pulse.Lib.Core.op_exists_Star PulseTutorial.LinkedList.node_ptr Pulse.Lib.Core.op_Star_Star FStar.Pervasives.Native.Some Pulse.Lib.Reference.pts_to PulseCore.FractionalPermission.full_perm PulseTutorial.LinkedList.Mknode PulseTutorial.LinkedList.is_list Pulse.Lib.Core.vprop
let rec is_list #t (x: llist t) (l: list t) : Tot vprop (decreases l) =
  
match l with
| [] -> pure (x == None)
| head :: tl ->
  exists* (p: node_ptr t) (tail: llist t).
    (pure (x == Some p) ** pts_to p ({ head = head; tail = tail })) ** is_list tail tl