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
flar.fst
module Flar

noeq
type flar (out:int) =
  | Flar : (int -> v:int{v = out}) -> flar out

val appFlar (#out:int) (f:flar out) (x:int) : v:int{v = out}
let appFlar #out f x = match f with
    | Flar f -> f x

val incr : #n:int -> f:(flar n) -> v:int{v = n + 1}
let incr #n f = (appFlar f 0) + 1

val test1 : v:int{v = 11}
let test1 = incr (Flar (fun x -> 10))
back to top