Inductive pair := K (n1 : nat) (n2 : nat -> nat). Definition snd (p : pair) : nat -> nat := match p with K _ f => f end.
Definition alias_K a b := K a b.
Fixpoint rec (x : nat) : nat := match x with 0 => 0 | S x => snd (K 0 rec) x end. Fixpoint rec_ko (x : nat) : nat := match x with 0 => 0 | S x => snd (alias_K 0 rec_ko) x end.
Endcase.
Modulefixpoint.
Inductive pair := K (n1 : nat) (n2 : nat -> nat). Definition snd (p : pair) : nat -> nat := match p with K _ f => f end.
Definition alias_K a b := K a b.
Fixpoint rec (x : nat) : nat := match x with 0 => 0 | S x => snd (K 0 rec) x end. Fixpoint rec_ko (x : nat) : nat := match x with 0 => 0 | S x => snd (alias_K 0 rec_ko) x end.
Fixpoint rec (x : nat) : nat := match x with 0 => 0 | S x => snd (K 0 rec) x end. Fixpoint rec_ko (x : nat) : nat := match x with 0 => 0 | S x => snd (alias_K 0 rec_ko) x end.
End primproj.
Messung V0.5
¤ Dauer der Verarbeitung: 0.12 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 und die Messung sind noch experimentell.
