Facebook
From Sludgy Lizard, 3 Years ago, written in Plain Text.
Embed
Download Paste or View Raw
Hits: 91
  1. (*
  2.   Inductive = pentru definirea noilor tipuri de date
  3.   Check = verificarea tipului
  4.   Definition = se foloseste pentru definirea functiilor (nerecursive)
  5.   Fixpoint = se foloseste pentru functii recursive
  6.   Compute = evaluarea functiilor
  7. *)
  8.  
  9.  
  10. Inductive natural : Type :=
  11.   | O
  12.   | S (n : natural).
  13.  
  14.  
  15. Fixpoint even (n : natural) : bool :=
  16.   match n with
  17.     | O => true
  18.     | S (O) => false
  19.     | S (S (m)) => even m
  20.   end.
  21.  
  22.  
  23. Compute (even (S (S (S (O))))).
  24.  
  25. Inductive weekday : Type :=
  26.   | Monday
  27.   | Tuesday
  28.   | Wednesday
  29.   | Thursday
  30.   | Friday
  31.   | Saturday
  32.   | Sunday.
  33.  
  34. Check (Saturday)
  35.  
  36.  
  37. Definition weekday_equal (d1 d2 : weekday) : bool :=
  38.   match d1, d2 with
  39.     | Monday, Monday => true
  40.     | Tuesday, Tuesday => true
  41.     (de completat cu restul de optiuni...)
  42.     | _, _ => false
  43.   end.
  44.  
  45.  
  46. Compute (weekday_equal Monday Tuesday).
  47.  
  48.  
  49.  
  50.  
  51.  
  52.  
  53.  
  54.  
  55.  
  56.  
  57.  
  58.  
  59.  
  60.  
  61.  
  62.  
  63.  
  64.