|
Set Universe Polymorphism.
Inductive D : nat -> Type :=
| DO : D O
| DS n : D n -> D (S n).
Fixpoint follow (n : nat) : D n -> Prop :=
match n with
| O => fun d => let 'DO := d in True
| S n' => fun d => (let 'DS _ d' := d in fun f => f d') (follow n')
end.
Definition step (n : nat) (d : D n) (H : follow n d) :
follow (S n) (DS n d)
:= H.
¤ 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.
|
