|
Require Import ssreflect.
Set Universe Polymorphism.
Cumulative Variant paths {A} (x:A) : A -> Type
:= idpath : paths x x.
Register paths as core.eq.type.
Register idpath as core.eq.refl.
Lemma case_test (b:bool) : paths b b.
Proof. case B:b; reflexivity. Qed.
¤ Dauer der Verarbeitung: 0.32 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.
|
