In Coq gibt es eine Hierarchie von Typen, von denen jeder den Typ des vorherigen angibt, d. H. Typ_0: Typ_1, Typ_1: Typ_2 und so weiter. In coqtop jedoch, wenn ich gebe ich Type : Type, die wie ein Widerspruch aussieht, aber nicht seit Type ist implizit indiziert.Explizite Typindizes in Coqtop aktivieren?
Frage: Wie kann die explizite Indizierung der Typ-Universen aktiviert werden?
Die kurze Antwort als @ejgallego oben erwähnt ist das Drucken von Universum Ebenen zu aktivieren:
Coq < Set Printing Universes.
Coq < Check Type.
[email protected]{Top.1}
: [email protected]{Top.1+1}
(* Top.1 |= *)
Konzeptionell gibt es in der Tat eine Hierarchie von Typen, die [email protected]{1}, [email protected]{2} usw. Allerdings Coq tatsächlich genannt werden könnten Unterhält Symbole für Universum Indizes und Beziehungen zwischen ihnen (Universum Einschränkungen) anstelle von expliziten Zahlen. Die Bedingungen werden konsistent gehalten, so dass es immer möglich ist, jedem Symbol eine eindeutige Zahl auf konsistente Weise zuzuweisen.
In der obigen Ausgabe können Sie sehen, dass Coq ein Universum Top.1 für die Type innerhalb der Befehl erstellt hat. Sein Typ ist immer eine Ebene höher, wobei Coq ohne ein weiteres Symbol mit dem Ausdruck Top.1+1 auskommt. Mit Set Printing Universes wird auch eine Liste von Constraints als Kommentar ausgegeben; in diesem Fall gibt es das eine Symbol im Kontext Top.1 und keine Einschränkungen auf der rechten Seite.
Coq verwaltet eine globale Liste von Universumsebenen und Einschränkungen, die bisher erstellt wurden. Sie können eine ausführlichere Erklärung der Universumsebenen und -beschränkungen in CPDT lesen: http://adam.chlipala.net/cpdt/html/Universes.html.
Sie möchten 'Set Printing Universen 'verwenden. – ejgallego