Fixpoint fib n := match n with
| O => 1
| 1 => 1
| S (S n as m) => fib n + fib m end.
(* In ored to compute implicit arguments the system has to whd this term. In call by name it takes a lot of time, in call by need it is
instantaneous. *) Definition statement k :=
(fun v => match v + v + v + v + v with 0 => True | _ => forall x, x + 1 = x end)
((fun x => x - x) (fib k)).
SetImplicitArguments.
Timeout 3 TimeAxiom test : statement 20.
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
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.
