|
Goal False /\ True.
Proof.
split.
idtac.
idtac.
exact I.
idtac.
idtac.
exact I.
Qed.
Lemma baz : (exists n, n = 3 /\ n = 3) /\ True.
Proof.
split. { eexists. split. par: trivial. }
trivial.
Qed.
Lemma baz1 : (True /\ False) /\ True.
Proof.
split. { split. par: trivial. }
trivial.
Qed.
Lemma foo : (exists n, n = 3 /\ n = 3) /\ True.
Proof.
split.
{ idtac.
unshelve eexists.
{ apply 3. }
{ split.
{ idtac. trivialx. }
{ reflexivity. } } }
trivial.
Qed.
Lemma foo1 : False /\ True.
Proof.
split.
{ exact I. }
{ exact I. }
Qed.
Definition banana := true + 4.
Check banana.
Lemma bar : (exists n, n = 3 /\ n = 3) /\ True.
Proof.
split.
- idtac.
unshelve eexists.
+ apply 3.
+ split.
* idtacx. trivial.
* reflexivity.
- trivial.
Qed.
Lemma baz2 : ((1=0 /\ False) /\ True) /\ False.
Proof.
split. split. split.
- solve [ auto ].
- solve [ trivial ].
- solve [ trivial ].
- exact 6.
Qed.
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
