|
Set Primitive Projections.
CoInductive stream (A : Type) := cons {
hd : A;
tl : stream A;
}.
CoFixpoint const {A} (x : A) := cons A x (const x).
Check (@eq_refl _ (const tt) <<: tl unit (const tt) = const tt).
¤ Dauer der Verarbeitung: 0.11 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.
|
