Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_6393.v Sprache: Coq

Original von: Coq^©

(* These always worked. *)
Goal prod True True. firstorder. Qed.
Goal True -> @sigT True (fun _ => True). firstorder. Qed.
Goal prod True True. dtauto. Qed.
Goal prod True True. tauto. Qed.

(* These should work. *)
Goal @sigT True (fun _ => True). dtauto. Qed.
(* These should work, but don't *)
(* Goal @sigT True (fun _ => True). firstorder. Qed. *)
(* Goal @sigT True (fun _ => True). tauto. Qed. *)

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Kontakt Drucken
Kontakt sprechenden Kalenders
in der Quellcodebibliothek suchen

schauen Sie vor die Tür

Fenster

Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.