ProofCafe01 のバックアップ差分(No.1)

• バックアップ一覧
• 現在との差分 を表示
• ソース を表示
• バックアップ を表示
• ProofCafe01 へ行く。
  • 1 (2010-04-03 (土) 16:31:04)

• 追加された行はこの色です。
• 削除された行はこの色です。

[[ocaml-nagoya]]

 Inductive list (A: Type) : Type :=
  | nil  : list A
  | cons : A -> list A -> list A.
 
 (* Check (cons nat 3 (nil nat)). *)
 
 Implicit Arguments nil [A].
 Implicit Arguments cons [A].
 (* Check (cons 3 nil). *)
 
 Fixpoint append {A : Type} (xs ys: list A) : list A :=
  match xs with
  | nil => ys
  | cons x xs => cons x (append xs ys)
  end.
 Infix "++" := append (at level 60).
 
 Fixpoint length {A : Type} (xs : list A) : nat :=
  match xs with
  | nil => O
  | cons x xs => S (length xs)
  end.
 
 Theorem append_assoc : forall (A: Type) (xs ys zs : list A),
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs).
 Proof.
  (* あなたの証明を書いてね *)
 Qed.
 
 Theorem append_length : forall (A: Type) (xs ys: list A),
   length (xs ++ ys) = length xs + length ys.
 Proof.
  (* あなたの証明を書いてね *)
 Qed.