| 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 692 B |
|
Quelle bug_4555.v Sprache: Coq |
|||||||||
|
Definition prod_map {A A' B B'} (f : A -> A') (g : B -> B')
(p : A * B) : A' * B' := (f (fst p), g (snd p)). Arguments prod_map {_ _ _ _} _ _ !_ /. Lemma test1 {A A' B B'} (f : A -> A') (g : B -> B') x y : prod_map f g (x,y) = (f x, g y). Proof. Succeed progress simpl; match goal with |- ?x = ?x => idtac end. (* LHS becomes (f x, g y) *) Succeed progress cbn; match goal with |- ?x = ?x => idtac end. (* LHS is not simplified *) Admitted. Axiom n : nat. Arguments Nat.add _ !_. Goal n + S n = 0. Fail progress cbn. Abort. Goal S n + S n = 0. progress cbn. match goal with |- S (n + S n) = 0 => idtac end. Abort. Goal S n + n = 0. Fail progress cbn. Abort. ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28