Quelle bug_16173.v Sprache: Coq

Section S.
  Variables (a:nat) (b:bool).

  Fail Set Default Proof Using ")".
  Fail Set Default Proof Using "a)".
  Fail Set Default Proof Using "(a . )".
  Fail Set Default Proof Using "(a .".
  Set Default Proof Using "".

  Lemma foo1 : True.
  Proof. trivial. Qed.

  Set Default Proof Using "()".
  Lemma foo2 : True.
  Proof. trivial. Qed.

  Set Default Proof Using "( )".
  Lemma foo2' : True.
  Proof. trivial. Qed.

  Set Default Proof Using "a b".
  Lemma foo3 : True.
  Proof. trivial. Qed.

  Set Default Proof Using "(b a)".
  Lemma foo4 : True.
  Proof. trivial. Qed.
End S.

Check foo1 : True.
Check foo2 : True.
Check foo2' : True.
Check foo3 : nat -> bool -> True.
Check foo4 : nat -> bool -> True.

Require Import Corelib.ssr.ssreflect.
(* ssr makes "\*\)" parse differently so preprocessing has to make sure to insert a space *)
Set Default Proof Using "Type*".

quality99%

¤ 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.