Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: NumeralNotationsNoLocal.v Sprache: Coq

Original von: Coq^©

(* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *)
Inductive unit11 := tt11.
Declare Scope unit11_scope.
Delimit Scope unit11_scope with unit11.
Goal True.
  evar (to_uint : unit11 -> Decimal.uint).
  evar (of_uint : Decimal.uint -> unit11).
  Fail Numeral Notation unit11 of_uint to_uint : uint11_scope.
  exact I.
  Unshelve.
  all: solve [ constructor ].
Qed.

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