Inductive S1a@{a} (A:typ@{a}) : Prop := with S1b (A:typ@{a}) : Prop :=
. (* Parameters should be syntactically the same for each inductive type. Type "S1a" has parameters "(A : typ@{a})" but type "S1b" has parameters "(A : typ@{a})".
*)
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.
