(* -*- coq-prog-args: ("-g") -*- *) Definition a := 0. #[ (* templatize *) universes( template) ] Inductive mysum (A B:Type) : Type :=
| myinl : A -> mysum A B
| myinr : B -> mysum A B.
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.
