@[simp] theorem list.is_prefix_refl (l : list α) : l <+: l :=
⟨[], by simp⟩

        \     /
        -------- (cons rule)
          \ /
   x::a    y::nlist
    \     /
    -------- (cons rule)
      \ / 
    cons x y :: nlist

inductive nlist: Type 
 | cons : a -> nlist -> nlist

good1 :: a -> b -> c -> nlist
good2 :: nlist
good3 :: a -> nlist

bad1 :: nlist -> nlist -> a -> nlist
bad2 :: nlist -> nlist

def take {α : Type} : ℕ → list α → list α
| 0       _         := []  --A,B
| (n + 1) []        := []  --C
| (n + 1) (x :: xs) := x :: take n xs --D

Proof
  ℕ=n-1
  list=[]
corresponds to 
Code
--            LHS  => RHS + IH             
| (k + 1) []        := []

inductive hypothesis is k,[] which corresponds to ℕ=n-1,list=[]

---------------------------------------------------
/-
typeclasses basically interfaces(which give polymorphism)  AKA methods will adapt to the type of the parameter. 
The set of allowable types is the Typeclass.  
eg. 
  fmap is the polymorphic method
  set of allowable types is {List,Maybe,Tree}
  This above set is a Typeclass called myFunctor  
  `[myFunctor List]` means "List ∈ myFunctor"
-/

/-
In lean typeclasses were annotated structures/records. 
Typeclasses are like interface classes in OO containing abstract methods
Classes that implement interfaces must also have 
virtual polymorphic methods to be implement the abstract class


-/

--1. typeclass which is similar to interface
class myFunctor (f: Type -> Type) :=
  fmap: (a-> b) -> (f a -> f b) --virtual method that needs to be implemented


--2. concrete method
def fmapList: (a -> b) -> (List a -> List b) :=
λ f => λ mylist => match mylist with 
| [] => []
| x::xs =>  [f x] ++ (fmapList f xs) 

--3. List implements the myFunctor interface
instance : myFunctor List where 
fmap := fmapList --bind concrete method to virtual method



def add2 : Nat -> Nat := λ x => x + 2

#reduce myFunctor.fmap add2 [1,3,5]

inductive Maybe (T : Type) :=
| Just : T -> Maybe T 
| Nil : Maybe T

open Maybe

def fmapMaybe: (a -> b) -> (Maybe a -> Maybe b) :=
λ f => λ mymaybe => match mymaybe with
| Nil => Nil
| Just (x:a) => Just (f x)

--`instance : myFunctor Maybe where` is an alternative syntax
instance : myFunctor Maybe := 
{
  fmap := fmapMaybe
}

#reduce myFunctor.fmap add2 (Just 3)
#reduce myFunctor.fmap add2 Nil

structure Point (T : Type) where 
  x : T 
  y : T

#check Point 
--Point : Type → Type
#check @Point.mk 
--@Point.mk : {T : Type} → T → T → Point T
#reduce Point.mk 4 5
--{ x := 4, y := 5 }
#check @Point.x 
--@Point.x : {T : Type} → Point T → T

/- Take notice of how structure Point gives us for free
Term Introduction function: Point.mk
Product Projection function: Point.x 
-/

namespace mytree 
universe u

inductive Tree (T: Type u) 
 | leaf : Tree T
 | node (left: Tree T) (key : Nat) (value: T) (right: Tree T) : Tree T 
  deriving Repr 


--Observe 2 different ways to define contains


--1st way: we bind the contains method to Tree datatype,
--behaves like a class method or a pointer receiver in golang
--or the `struct` `impl` pattern in Rust
def Tree.contains (t: Tree T) (k : Nat) : Bool := 
  match t with 
  | leaf => false 
  | node left key value right => 
    if k < key then 
      left.contains k --notice using dot operator, 1st argument is omitted
    else if key < k then 
      right.contains k
    else
      true


--2nd way: a normal function
def contains (t: Tree T) (k : Nat) : Bool := 
  match t with 
  | Tree.leaf => false 
  | Tree.node left key value right => 
    if k < key then 
      contains left k
    else if key < k then 
      contains right k
    else
      true

end mytree