| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/success/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 418 B |
|
Quelle NumberNotationsNoLocal.vSprache: Coq |
|||||||||||||||
|
(* Test that number notations don't work on proof-local variables, especially not ones contai 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 Number Notation unit11 of_uint to_uint : uint11_scope. exact I. Unshelve. all: solve [ constructor ]. Qed.
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09