We are hiring ! See our job offers.
swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
Raw File
Tip revision: f94b06de7edcb61d3c49f19417e53dc7dc21d552 authored by Anish Tondwalkar on 22 June 2021, 08:13:54 UTC
updated README
Tip revision: f94b06d
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)
back to top