Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
coqbugs0266.v
Sprache: Unknown
(* It is forbidden to erase a variable (or a local def) that is used in
the current goal. *)
Section S.
Let a := 0.
Definition b := a.
Goal b = b.
Fail clear a.
Abort.
End S.
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|