Random lean code

leansandbox.lean

def hello := "world"

open List

#check Nat.zero
#check Nat.succ
#check Nat.succ 0
#check Nat.add
#check Nat.add 1
#check Nat.add 2 2
#check List.filter
#check List.filter (λ x => x < 10)

def f (l: List Nat): List Nat :=
  List.filter (λ x => x < 10) l

def f': List Nat → List Nat :=
  List.filter (λ x => x < 10)

def f'' := List.filter (λ x => x < 10)

def divisible (n m: Nat) : Bool := n % m = 0

structure PosNat where
  numerator: Nat
  denominator: Nat

inductive Maybe (α: Type) where
  | Nothing
  | Just: α → Maybe α 

def natDivTo (n m: Nat): Type 0 :=
  if divisible n m then Nat else PosNat

def natDivTo' (n m: Nat): Maybe Nat :=
  if divisible n m then
    Maybe.Just (n / m)
  else
    Maybe.Nothing

#eval 2 + (if 4 > 5 then 10 else 5)

def baz: Nat := 
  let x := natDivTo' 12 3
  match x with
  | Maybe.Nothing => 0
  | Maybe.Just x' => x'

inductive Either (α: Type) (β: Type) where
| Left: α → Either α β 
| Right: β → Either α β 

inductive Result (α: Type) where
| Error: String → Result α  
| OK: α → Result α

#check divisible

#eval f [0, 5, 10, 15]
#eval f' [0, 5, 10, 15]
#eval f'' [0, 5, 10, 15]

def addOne: Nat → Nat := Nat.add 1

def sum (l: List Nat): Nat :=
  --foldr (λ i acc => i + acc) 0 l
  foldr Nat.add 0 l

class Summable (α : Type) where
  plus: α → α → α 
  origin: α

instance : Summable Nat where
  plus := Nat.add
  origin := 0

def sum' [Summable α] (l: List α): α :=
  foldr Summable.plus Summable.origin l

def upTo (n: Nat): List Nat := drop 1 (range n)

def divisors (n: Nat) := filter (divisible n) (upTo n)

#eval divisors 8

def sumOfDivisors (n: Nat): Nat := sum' (divisors n)

#eval sumOfDivisors 6

def even (n: Nat): Bool := n % 2 = 0

def odd (n: Nat): Bool := n % 2 = 1

def prime (n: Nat): Bool :=
  n > 1 && length (divisors n) = 1

def perfect (n: Nat): Bool :=
  sumOfDivisors n = n

def abundant (n: Nat): Bool :=
  sumOfDivisors n > n

def powerlist (l: List α): List (List α) :=
  match l with
  | nil => [nil]
  | (n :: ns) => 
    let p := powerlist ns
    List.append p (map (cons n) p)

#eval powerlist [6, 4, 9, 12]

def semiperfect (n: Nat): Bool :=
  any (powerlist (divisors n)) (λ l => sum l = n)

def weird (n: Nat): Bool :=
  abundant n && not (semiperfect n)

#eval weird 70