Revision 5963c0edc394e063fc9e58b3330288446c61a4da authored by mkolosick on 23 April 2020, 23:57:54 UTC, committed by mkolosick on 23 April 2020, 23:57:54 UTC
1 parent 5a23fd2
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)
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...