fork download
  1. let sum = \(l : List Natural) ->
  2. List/fold Natural l Natural (
  3. \(x : Natural) -> \(s : Natural) ->
  4. x + s
  5. ) 0
  6. let equals = \(a : Natural) -> \(b: Natural) ->
  7. let da = Natural/subtract b a
  8. let db = Natural/subtract a b
  9. in Natural/isZero (da + db)
  10. let filter = \(t : Type) -> \(p : t -> Bool) -> \(l : List t) ->
  11. List/fold t l (List t) (
  12. \(x : t) -> \(xs : List t) ->
  13. xs # (if p x then [x] else [] : List t)
  14. ) ([] : List t)
  15. let divides = \(b : Natural) -> \(a : Natural) ->
  16. True != Natural/isZero (Natural/fold a Natural (
  17. \(x : Natural) ->
  18. let d = Natural/subtract b x
  19. let e = Natural/subtract x b
  20. in if Natural/isZero (d + e) then x else d
  21. ) a)
  22. let enumerate = \(n : Natural) ->
  23. let r = Natural/fold n {n : Natural, l : List Natural} (
  24. \(x : {n : Natural, l : List Natural}) ->
  25. {n = (x.n + 1), l = x.l # [x.n]}
  26. ) ({n = 1, l = [] : List Natural})
  27. in r.l
  28. let factor = \(n : Natural) -> filter Natural (\(x : Natural) -> divides x n) (enumerate n)
  29. let perfect = \(n : Natural) ->
  30. equals (sum (factor n)) (n * 2)
  31. in filter Natural perfect (enumerate 100)
Not running #stdin #stdout 0s 0KB
stdin
Standard input is empty
stdout
Standard output is empty