(*
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).
{"html5":"htmlmixed","css":"css","javascript":"javascript","php":"php","python":"python","ruby":"ruby","lua":"text\/x-lua","bash":"text\/x-sh","go":"go","c":"text\/x-csrc","cpp":"text\/x-c++src","diff":"diff","latex":"stex","sql":"sql","xml":"xml","apl":"apl","asterisk":"asterisk","c_loadrunner":"text\/x-csrc","c_mac":"text\/x-csrc","coffeescript":"text\/x-coffeescript","csharp":"text\/x-csharp","d":"d","ecmascript":"javascript","erlang":"erlang","groovy":"text\/x-groovy","haskell":"text\/x-haskell","haxe":"text\/x-haxe","html4strict":"htmlmixed","java":"text\/x-java","java5":"text\/x-java","jquery":"javascript","mirc":"mirc","mysql":"sql","ocaml":"text\/x-ocaml","pascal":"text\/x-pascal","perl":"perl","perl6":"perl","plsql":"sql","properties":"text\/x-properties","q":"text\/x-q","scala":"scala","scheme":"text\/x-scheme","tcl":"text\/x-tcl","vb":"text\/x-vb","verilog":"text\/x-verilog","yaml":"text\/x-yaml","z80":"text\/x-z80"}