| 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 556 B |
|
Quelle bug_3210.v Sprache: Coq |
|||||||||
|
(* Test support of let-in in arity of inductive types *)
Inductive Foo : let X := Set in X := | I : Foo. Definition foo (x : Foo) : bool := match x with I => true end. Definition foo' (x : Foo) : x = x. case x. match goal with |- I = I => idtac end. (* check form of the goal *) Undo 2. elim x. match goal with |- I = I => idtac end. (* check form of the goal *) Undo 2. induction x. match goal with |- I = I => idtac end. (* check form of the goal *) Undo 2. destruct x. match goal with |- I = I => idtac end. (* check form of the goal *) Abort. ¤ Dauer der Verarbeitung: 0.5 Sekunden ¤*© Formatika GbR, Deutschland |
|
2026-03-28