Fixpoint demo_recursion(n:nat) := match n with
|0 => Type
|S k => (demo_recursion k) -> Type end.
Record Demonstration := mkDemo
{
demo_law : forall n:nat, demo_recursion n;
demo_stuff : forall n:nat, forall q:(fix demo_recursion (n : nat) : Type := match n with
| 0 => Type
| S k => demo_recursion k -> Type end) n, (demo_law (S n)) q
}.
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.
