Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: SuggestProofUsing.v Sprache: Coq

Original von: Coq^©

Set Suggest Proof Using.

Section Sec.
  Variables A B : Type.

  (* Some normal lemma. *)
  Lemma nat : Set.
  Proof.
    exact nat.
  Qed.

  (* Make sure All is suggested even though we add an unused variable
  to the context. *)
  Let foo : Type.
  Proof.
    exact (A -> B).
  Qed.

  (* Having a [Proof using] disables the suggestion message. *)
  Definition bar : Type.
  Proof using A.
    exact A.
  Qed.

  (* Transparent definitions don't get a suggestion message. *)
  Definition baz : Type.
  Proof.
    exact A.
  Defined.

End Sec.

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