Quelle PrintCanonicalProjections.v Sprache: Coq

Record TYPE := Pack_TYPE { sort_TYPE :> Type }.
Record eqType := Pack_eq { sort_eq :> Type; _ : sort_eq -> sort_eq -> bool }.

Definition eq_op (T : eqType) : T -> T -> bool :=
  match T with Pack_eq _ op => op end.

Definition bool_eqb b1 b2 :=
  match b1, b2 with
  | false, false => true
  | true, true => true
  | _, _ => false
  end.

Canonical bool_TYPE := Pack_TYPE bool.
Canonical bool_eqType := Pack_eq bool bool_eqb.

Canonical nat_TYPE := Pack_TYPE nat.
Canonical nat_eqType := Pack_eq nat Nat.eqb.

Definition prod_eqb (T U : eqType) (x y : T * U) :=
  match x, y with
  | (x1, x2), (y1, y2) =>
    andb (eq_op _ x1 y1) (eq_op _ x2 y2)
  end.

Canonical prod_TYPE (T U : TYPE) := Pack_TYPE (T * U).
Canonical prod_eqType (T U : eqType) := Pack_eq (T * U) (prod_eqb T U).

Definition sum_eqb (T U : eqType) (x y : T + U) :=
  match x, y with
  | inl x, inl y => eq_op _ x y
  | inr x, inr y => eq_op _ x y
  | _, _ => false
  end.

Canonical sum_TYPE (T U : TYPE) := Pack_TYPE (T + U).
Canonical sum_eqType (T U : eqType) := Pack_eq (T + U) (sum_eqb T U).

Print Canonical Projections bool.
Print Canonical Projections nat.
Print Canonical Projections prod.
Print Canonical Projections sum.
Print Canonical Projections sort_TYPE.
Print Canonical Projections sort_eq.
Print Canonical Projections sort_TYPE bool.
Print Canonical Projections bool_eqType.

quality100%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.