(*
  Inductive = pentru definirea noilor tipuri de date
  Check = verificarea tipului
  Definition = se foloseste pentru definirea functiilor (nerecursive)
  Fixpoint = se foloseste pentru functii recursive
  Compute = evaluarea functiilor
*)


Inductive natural : Type := 
  | O
  | S (n : natural).


Fixpoint even (n : natural) : bool :=
  match n with
    | O => true
    | S (O) => false
    | S (S (m)) => even m
  end.


Compute (even (S (S (S (O))))).

Inductive weekday : Type :=
  | Monday
  | Tuesday
  | Wednesday
  | Thursday
  | Friday
  | Saturday
  | Sunday.

Check (Saturday)


Definition weekday_equal (d1 d2 : weekday) : bool := 
  match d1, d2 with
    | Monday, Monday => true
    | Tuesday, Tuesday => true
    (de completat cu restul de optiuni...)
    | _, _ => false
  end.


Compute (weekday_equal Monday Tuesday).