| products/Sources/formale Sprachen/C/LibreOffice/solenv/ (LibreOffice Version 25.8.3.2©) Datei vom 5.10.2025 mit Größe 746 B |
|
SSL 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.9 Sekunden (vorverarbeitet am 2026-09-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-10-10