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
incrState.fst
module IncrState

noeq
type hst (state:Type) (a:Type) (p q:state) =
  | State : (state -> (a & state)) -> hst state a p q

assume val pure (#state:Type) (#a:Type) (#w:state) (x:a) : hst state a w w
assume val bind (#state:Type) (#a #b:Type) (#w1 #w2 #w3:state)
  (f:hst state a w1 w2) (g:a -> hst state b w2 w3) : hst state b w1 w3


let get (#state:Type) (#w:state) : hst state state w w =
  State (fun _ -> w, w)

let set (#state:Type) (#w:state) (w1:state) : hst state unit w w1 =
  State (fun _ -> (), w1)

let fresh (#n:int) : hst int int n (n + 1) =
  get `bind` (fun _ -> set (n + 1) `bind` (fun _ -> pure n))
back to top