Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: script.js Sprache: Coq

Original von: Coq^©

(* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *)
Goal forall (P : SProp), P -> P.
Proof.
  intros P H. set (H0 := H).
  (* goal is now H0 *)
  exact H0.
Qed.

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Kontakt Drucken
Kontakt sprechenden Kalenders
Eigene Datei ansehen

schauen Sie vor die Tür

Fenster

Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.