gistfile1.txt

(* This is coq *)
Print nat.
Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Fixpoint plus (m n : nat) {struct m} : nat :=
  match m with
    | O    => n
    | S m' => S (plus m' n)
end.
Print plus.
Check plus O O.
Check plus (S O) O.
Check plus (S (S (S O))) (S O).
Eval compute in plus  (S (S (S O))) (S O).

(*
Parameter mult  : nat -> nat -> nat.
Eval compute in mult (S O) (S O).
*)

Check S.
Check plus.
Check S.



Fixpoint mult (m n : nat) : nat :=
  match m with
    | O     => O
    | S m'   => (plus n (mult m' n))
  end
.

Check mult O O.
Check mult (S O) O.
Check mult O (S O).

Eval compute in mult O O.
Eval compute in mult (S (S O)) (S O).

Eval compute in mult O (S O).
Eval compute in mult (S O) O.

ガリグ先生のテキストの演習