| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 412 B |
|
Quelle bug_9532.v Sprache: Coq |
|||||||||
|
Declare Custom Entry atom.
Notation "1" := tt (in custom atom). Notation "atom:( s )" := s (s custom atom). Declare Custom Entry expr. Notation "expr:( s )" := s (s custom expr). Notation "( x , y , .. , z )" := (@cons unit x (@cons unit y .. (@cons unit z (@nil unit)) ..)) (in custom expr at level 0, x custom atom, y custom atom, z custom atom). Check atom:(1). Check expr:((1,1)). Check expr:((1,1,1)). ¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28