products/sources/formale sprachen/PVS/groups/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: idtac.out   Sprache: Coq

Original von: Coq©
Require Import Coq.Unicode.Utf8.

Section test.
Context (very_very_long_type_name1 : Type) (very_very_long_type_name2 : Type).
Context (f : very_very_long_type_name1 -> very_very_long_type_name2 -> Prop).

Lemma test : True -> True ->
  forall (x : very_very_long_type_name1) (y : very_very_long_type_name2),
    f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y.
Proof. Show. Abort.

Lemma test : True -> True ->
  forall (x : very_very_long_type_name2) (y : very_very_long_type_name1)
         (z : very_very_long_type_name2),
    f y x /\ f y z.
Proof. Show. Abort.

Lemma test : True -> True ->
  forall (x : very_very_long_type_name2) (y : very_very_long_type_name1)
         (z : very_very_long_type_name2),
    f y x /\ f y z /\ f y x /\ f y z /\ f y x /\ f y z.
Proof. Show. Abort.

Lemma test : True -> True ->
  exists (x : very_very_long_type_name1) (y : very_very_long_type_name2),
    f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y.
Proof. Show. Abort.
End test.

¤ Dauer der Verarbeitung: 0.16 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.


Bot Zugriff