Inductive Acc (x: A) : SProp :=
Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. destruct 1; trivial. Defined.
GlobalArguments Acc_inv [x] _ [y] _, [x] _ y _.
Fail Polymorphic Definition Fix_F@{s;u|} (P:A -> Type@{s;u}) (F:forall {x:A}, (forall y:A, R y x -> P y) -> P x)
:= fix Fix_F {x:A} (a:Acc x) {struct a} : P x :=
F (fun (y:A) (h:R y x) => Fix_F (Acc_inv a h)).
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.
