SSL bug_12895.v Sprache: Coq

Fixpoint bug_1 (e1 : nat) {struct e1}
  : nat
with bug_2 {H_imp : nat} (e2 : nat) {struct e2}
  : nat.
Proof.
  - exact e1.
  - exact e2.
Admitted.

Fixpoint hbug_1 (a:bool) (e1 : nat) {struct e1}
  : nat
with hbug_2 (a:nat) (e2 : nat) {struct e2}
  : nat.
Proof.
  - exact e1.
  - exact e2.
Admitted.

Check (hbug_1 : bool -> nat -> nat).
Check (hbug_2 : nat -> nat -> nat).

quality99%

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