|
(* Are recursively non-uniform params correctly treated? *)
Inductive list (A:nat -> Type) n := cons : A n -> list A (S n) -> list A n.
Inductive term n := app (l : list term n).
Definition term_list :=
fix term_size n (t : term n) (acc : nat) {struct t} : nat :=
match t with
| app _ l =>
(fix term_list_size n (l : list term n) (acc : nat) {struct l} : nat :=
match l with
| cons _ _ t q => term_list_size (S n) q (term_size n t acc)
end) n l (S acc)
end.
¤ Dauer der Verarbeitung: 0.13 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.
|
