| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/stm/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 343 B |
|
Quelle delayed_restrict_univs_9093.v Sprache: Coq |
|||||||||||||||
|
(* -*- coq-prog-args: ("-async-proofs" "on"); -*- *) Unset Universe Polymorphism. Ltac exact0 := let x := constr:(Type) in exact 0. Lemma lemma_restrict_abstract@{} : (nat * nat)%type. Proof. split;[exact 0|abstract exact0]. Qed. (* Debug: 10237:proofworker:0:0 STM: sending back a fat state Error: Universe {polymorphism.1} is unbound. *)
¤ Dauer der Verarbeitung: 0.2 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-04-04