-- This file:
--   http://anggtwu.net/LEAN/overloaded1.lean.html
--   http://anggtwu.net/LEAN/overloaded1.lean
--          (find-angg "LEAN/overloaded1.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LEAN/overloaded1.lean"))
-- (find-fplean4page 101 "Overloading and Type Classes")
-- (find-fplean4text 101 "Overloading and Type Classes")
-- (find-fplean4page 105 "open Plus (plus)")
-- (find-fplean4text 105 "open Plus (plus)")
-- (find-fplean4page 105 "Overloaded Addition")
-- (find-fplean4text 105 "Overloaded Addition")
-- (find-fplean4page 106 "Conversion to Strings")
-- (find-fplean4text 106 "Conversion to Strings")

inductive Pos : Type where
  | one : Pos
  | succ : Pos → Pos

-- def seven : Pos := 7

def seven : Pos :=
  Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))

class Plus (α : Type) where
  plus : α → α → α

instance : Plus Nat where
  plus := Nat.add

open Plus (plus)

#eval plus 5 3


def Pos.plus : Pos → Pos → Pos
  | Pos.one, k => Pos.succ k
  | Pos.succ n, k => Pos.succ (n.plus k)

instance : Plus Pos where
  plus := Pos.plus

def fourteen : Pos := plus seven seven

-- #eval plus 5.2 917.25861

instance : Add Pos where
  add := Pos.plus

-- def fourteen : Pos := seven + seven

def posToString (atTop : Bool) (p : Pos) : String :=
  let paren s := if atTop then s else "(" ++ s ++ ")"
  match p with
  | Pos.one => "Pos.one"
  | Pos.succ n => paren s!"Pos.succ {posToString false n}"


instance : ToString Pos where
  toString := posToString true

#eval s!"There are {seven}"

def Pos.toNat : Pos → Nat
  | Pos.one => 1
  | Pos.succ n => n.toNat + 1

instance : ToString Pos where
  toString x := toString (x.toNat)

#eval s!"There are {seven}"



def Pos.mul : Pos → Pos → Pos
  | Pos.one, k => k
  | Pos.succ n, k => n.mul k + k

instance : Mul Pos where
  mul := Pos.mul

#eval [seven * Pos.one,
       seven * seven,
       Pos.succ Pos.one * seven]

-- class OfNat (α : Type) (_ : Nat) where
--   ofNat : α


-- [7, 49, 14]

----------------------------------------

class ToLuaTree (α : Type) where
  toLuaTree : α → String

instance : ToLuaTree String where
  toLuaTree s := "\"" ++ s ++ "\""

#check ToLuaTree
#check ToLuaTree.toLuaTree
#eval  ToLuaTree.toLuaTree "foo"



-- Local Variables:
-- coding:  utf-8-unix
-- End: