|
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
}.
Theorem DemoError : Demonstration.
Fail apply mkDemo. (*Anomaly: Uncaught exception Not_found. Please report.*)
Abort.
¤ Dauer der Verarbeitung: 0.15 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.
|
