Skip to content

Instantly share code, notes, and snippets.

@alcides
Created December 5, 2021 11:54
Show Gist options
  • Save alcides/9fe28137561cca3fb708d1cb2ea8eeda to your computer and use it in GitHub Desktop.
Save alcides/9fe28137561cca3fb708d1cb2ea8eeda to your computer and use it in GitHub Desktop.
Lean benchmarks
def countPairs (xm ym:Nat) : IO Nat := do
let mut count := 0
for x in [0:xm+1] do
for y in [0:ym+1] do
count := if x == y then count + 1 else count
return count
def main (args : List String) : IO UInt32 :=
do
let xmax := 10000
let ymax := 10000
let c <- countPairs xmax ymax
IO.println c
return 0
partial def makePairs (ymax x y:Nat) : List (Nat × Nat) :=
(x, y) :: match (x, y) with
| (0, 0) => []
| (x, 0) => makePairs ymax (x-1) ymax
| (x, y) => makePairs ymax x (y-1)
def main (args : List String) : IO UInt32 :=
do
let xmax := 10000
let ymax := 10000
let ps := makePairs ymax xmax ymax
let fn := ps.filter (λ(x, y)=> x == y)
IO.println fn.length
return 0
partial def makePairs (ymax x y:Nat) (l:List (Nat × Nat)) : List (Nat × Nat) :=
match (x, y) with
| (0, 0) => (x, y) :: l
| (x, 0) => makePairs ymax (x-1) ymax ((x, y)::l)
| (x, y) => makePairs ymax x (y-1) ((x, y)::l)
def main (args : List String) : IO UInt32 :=
do
let xmax := 10000
let ymax := 10000
let ps := makePairs ymax xmax ymax []
let fn := ps.filter (λ(x, y)=> x == y)
IO.println fn.length
return 0
Real time using UNIX time on a 2016 Macbook Pro with 2,9 GHz Dual-Core Intel Core i5
matrix_slow.lean Stack Overflow
matrix_tailrec.lean 58.35s
matrix_forin.lean 53.22s
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment