Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_1448.v Sprache: Coq

Original von: Coq^©

Require Import Relations.
Require Import Setoid.
Require Import Ring_theory.
Require Import Ring_base.

Variable R : Type.
Variable Rone Rzero : R.
Variable Rplus Rmult Rminus : R -> R -> R.
Variable Rneg : R -> R.

Lemma my_ring_theory : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq
R).
Admitted.

Variable Req : R -> R -> Prop.

Hypothesis Req_refl : reflexive _ Req.
Hypothesis Req_sym : symmetric _ Req.
Hypothesis Req_trans : transitive _ Req.

Add Relation R Req
  reflexivity proved by Req_refl
  symmetry proved by Req_sym
  transitivity proved by Req_trans
  as Req_rel.

Add Ring my_ring : my_ring_theory (abstract).

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.