Quelle if.v Sprache: 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.

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.