47 lines
1.1 KiB
Text
47 lines
1.1 KiB
Text
#check @Array.mk
|
|
|
|
def v : Array Nat := @Array.mk Nat 10 (fun ⟨i, _⟩ => i)
|
|
|
|
def w : Array Nat :=
|
|
(mkArray 9 1).push 3
|
|
|
|
def f : Fin w.sz → Nat :=
|
|
Array.casesOn w (fun _ f => f)
|
|
|
|
def arraySum (a : Array Nat) : Nat :=
|
|
a.foldl Nat.add 0
|
|
|
|
#eval mkArray 4 1
|
|
#eval Array.map (fun x => x+10) v
|
|
#eval f ⟨1, sorry⟩
|
|
#eval f ⟨9, sorry⟩
|
|
#eval (((mkArray 1 1).push 2).push 3).foldl (fun x y => x + y) 0
|
|
#eval arraySum (mkArray 10 1)
|
|
axiom axLt {a b : Nat} : a < b
|
|
#eval (mkArray 10 1).data ⟨1, axLt⟩ + 20
|
|
#eval (mkArray 10 1).data ⟨2, axLt⟩
|
|
#eval (mkArray 10 3).data ⟨2, axLt⟩
|
|
|
|
#eval #[1, 2, 3].insertAt 0 10
|
|
#eval #[1, 2, 3].insertAt 1 10
|
|
#eval #[1, 2, 3].insertAt 2 10
|
|
#eval #[1, 2, 3].insertAt 3 10
|
|
#eval #[].insertAt 0 10
|
|
|
|
def tst1 : IO Unit :=
|
|
#[1, 2, 3, 4].forRevM IO.println
|
|
|
|
#eval tst1
|
|
|
|
#eval #[1, 2].extract 0 1
|
|
#eval #[1, 2].extract 0 0
|
|
#eval #[1, 2].extract 0 2
|
|
|
|
#eval #[1, 2, 3, 4].filterMap fun x => if x % 2 == 0 then some (x + 10) else none
|
|
|
|
def tst : IO (List Nat) :=
|
|
[1, 2, 3, 4].filterMapM fun x => do
|
|
IO.println x;
|
|
if x % 2 == 0 then pure $ some (x + 10) else pure none
|
|
|
|
#eval tst
|