Some simple arithmetic in Lean4

Arith.lean

instance FloatHasNeg : HasNeg Float := ⟨λ x => 0 - x⟩
instance HasPowFloatNat : HasPow Float Nat := ⟨λ x y => x ^ (y.toFloat)⟩


def addNats : Nat → Nat → Nat
| x, y => x + y

def addInts : Int → Int → Int
| x, y => x + y

-- N.B., no signed bounded Int types currently
def addUInt64s : UInt64 → UInt64 → UInt64
| x, y => x + y

-- N.B., Float = 64bit float
def addFloats : Float → Float → Float
| x, y => x + y

def quadraticFormula (a b c: Float) : (Float × Float) :=
let ans1 := (-b + (b ^ 2 - 4 * a * c).sqrt) / (2 * a);
let ans2 := (-b - (b ^ 2 - 4 * a * c).sqrt) / (2 * a);
(ans1, ans2)


def main : IO Unit := do
IO.println (addNats 0 1);
IO.println (addInts 0 1);
IO.println (addUInt64s 0 1);
IO.println (addFloats 0 1);
IO.println (quadraticFormula 1 (-2) (-3));
pure ()