Module Short. Set Universe Polymorphism. Inductive relevant (A : Type) (B : Type) : Prop := . Section foo. Variables A B : Type. Definition foo := prod (relevant A B) A. End foo.
Section bar. Variable A : Type. Variable B : Type. Definition bar := prod (relevant A B) A. End bar.
Set Printing Universes. Check bar nat Set : Set. (* success *) Check foo nat Set : Set. (* Toplevel input, characters 6-17: Error:
The term "foo (* Top.303 Top.304 *) "Type (* Top.304 *)" while it is expected to have type "Set" (Universe inconsistency: Cannot enforce Top.304 = Set because Set
< Top.304)). *) End Short.
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.
