| 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 471 B |
|
Quelle bug_5159.v Sprache: Coq |
|||||||||
|
Axiom foo : Type.
Definition bar := 1. Definition bar' := Eval cbv -[bar] in bar. Declare Reduction red' := cbv -[bar]. Opaque bar. Definition bar'' := Eval red' in bar. Declare Reduction red'' := cbv -[bar]. (* Error: Cannot coerce bar to an evaluable reference. *) Definition bar''' := Eval cbv -[bar] in bar. (* Error: Cannot coerce bar to an evaluable reference. *) Definition foo' := Eval cbv -[foo] in foo. (* Error: Cannot coerce foo to an evaluable reference. *) ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28