Commit 85bb06ef authored by Andrei Paskevich's avatar Andrei Paskevich

example of multiple assignment

parent bdec33a5
type uref = { mutable cnt : int }
type dref = { mutable urf : uref }
type tref = { mutable drf : dref }
let che (t t1: tref) (d : dref)
ensures { t.drf.urf.cnt = 1 /\ t1.drf.urf.cnt = 0 }
= (t.drf, d.urf, t.drf.urf, t1.drf) <- (d, {cnt = 1}, {cnt = 0}, t.drf)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment