swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
Tip revision: b6407e0f026cf5491ca5ed0a35ea5cf316ebe8ca authored by Anish Tondwalkar on 21 May 2021, 03:15:25 UTC
formatted for submission
formatted for submission
Tip revision: b6407e0
tick-append-ghost.fst
module TickAppend
open FStar.Ref
val length: list 'a -> Tot nat
let rec length l = match l with
| [] -> 0
| _ :: tl -> 1 + length tl
val n : ref int
let n = ST.alloc 0
let step _ =
let n0 = read n in
write n (n0 + 1)
val append : xs:list 'a -> ys:list 'a ->
ST (list 'a)
(fun _ -> True)
(fun h0 _ h1 -> sel h1 n = sel h0 n + length xs)
let rec append xs ys =
match xs with
| [] -> ys
| x :: xs -> step (); x :: (append xs ys)