Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Scheme.v Sprache: Coq

Original von: Coq^©

(* This failed in 8.3pl2 *)

Scheme Induction for eq Sort Prop.
Check eq_ind_dep.

(* This was broken in v8.5 *)

Set Rewriting Schemes.
Inductive myeq A (a:A) : A -> Prop := myrefl : myeq A a a.
Unset Rewriting Schemes.

Check myeq_rect.
Check myeq_ind.
Check myeq_rec.
Check myeq_congr.
Check myeq_sym_internal.
Check myeq_rew.
Check myeq_rew_dep.
Check myeq_rew_fwd_dep.
Check myeq_rew_r.
Check internal_myeq_sym_involutive.
Check myeq_rew_r_dep.
Check myeq_rew_fwd_r_dep.

Set Rewriting Schemes.
Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true.
Unset Rewriting Schemes.

¤ Dauer der Verarbeitung: 0.14 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.