| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/output/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 235 B |
|
Quelle names.v Sprache: Coq |
|||||||||||||||
|
(* Test no clash names occur *) (* see bug #2723 *) Parameter a : forall x, {y:nat|x=y}. Fail Definition b y : {x:nat|x=y} := a y. Goal (forall n m, n <= m -> m <= n -> n = m) -> True. intro H; epose proof (H _ 3) as H. Show. Abort.
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-04-04