|
Fixpoint arrow (n: nat) :=
match n with
| S n => bool -> arrow n
| O => bool
end.
Fixpoint apply (n : nat) : arrow n -> bool :=
match n return arrow n -> bool with
| S n => fun f => apply _ (f true)
| O => fun x => x
end.
Axiom f : arrow 10000.
Definition v : bool := Eval compute in apply _ f.
Definition w : bool := Eval vm_compute in v.
¤ Dauer der Verarbeitung: 0.14 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.
|
