Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: if.v Sprache: Coq

Original von: Coq^©

(* The synthesis of the elimination predicate may fail if algebraic *)
(* universes are not cautiously treated *)

Check (fun b : bool => if b then Type else nat).

(* Check correct use of if-then-else predicate annotation (cf BZ#690) *)

Check fun b : bool =>
if b as b0 return (if b0 then b0 = true else b0 = false)
then refl_equal true
else refl_equal false.

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