max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/playground/persistentarray): fix test

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-31 16:02:21 -07:00
parent 46f361daab
commit fe9908cad3
1 changed files with 11 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
tests/playground/persistentarray.lean
View file

@ -4,25 +4,25 @@ abbrev MyArray := PersistentArray Nat
-- abbrev MyArray := Array Nat
def mkMyArray (n : Nat) : MyArray :=
n.fold (λ i s, s.push i) { PersistentArray . }
n.fold (λ i s => s.push i) { PersistentArray . }
-- n.fold (λ i s, s.push i) Array.empty
def check (n : Nat) (p : Nat → Nat → Bool) (s : MyArray) : IO Unit :=
n.mfor $ λ i, unless (p i (s.get i)) (throw (IO.userError ("failed at " ++ toString i ++ " " ++ toString (s.get i))))
n.mfor $ λ i => unless (p i (s.get i)) (throw (IO.userError ("failed at " ++ toString i ++ " " ++ toString (s.get i))))
def inc1 (n : Nat) (s : MyArray) : MyArray :=
n.fold (λ i s, s.set i (s.get i + 1)) s
n.fold (λ i s => s.set i (s.get i + 1)) s
def checkId (n : Nat) (s : MyArray) : IO Unit :=
check n (==) s
check n (fun a b => a == b) s
def main (xs : List String) : IO Unit :=
do
let n := xs.head.toNat,
let t := mkMyArray n,
checkId n t,
let t := inc1 n t,
check n (λ i v, v == i + 1) t,
IO.println t.size,
IO.println t.stats,
let n := xs.head.toNat;
let t := mkMyArray n;
checkId n t;
let t := inc1 n t;
check n (λ i v => v == i + 1) t;
IO.println t.size;
IO.println t.stats;
pure ()