Coq: libérer des univers

Existe-t-il un moyen de créer des univers Reset (ou plus généralement, libres) dans Coq?Coq: libérer des univers

Universe M. 
Print Sorted Universes. (*M = Type.2*) 
Fail Print M. (*Error: M not a defined object.*) 
Reset M. 
Print Sorted Universes. (*M = Type.2*) 
Definition M := [email protected]{M}. 
Print M. (*M = Type: Type*) 
Print Sorted Universes. (*M = Type.2*) 
Reset M. 
Fail Print M. (*Error: M not a defined object.*) 
Print Sorted Universes. (*M = Type.2*)

Tout ce que je fais, M = Type.2. Je suis en Coq 8,5

Source

2017-03-18 jaam

Je crains que je ne connais pas 8,5 codebase de savoir ce qui est possible là-bas, 8.6 a une nouvelle implémentation de l'univers de vérification si YMMV. – ejgallego

@ejgallego: Est-ce que 'Universe M. Reset M.' efface l'univers en 8.6? – jaam

Je ne sais pas, mais il affiche l'avertissement: 'Réinitialiser pas mis en œuvre pour les constantes générées automatiquement – ejgallego

J'ai trouvé 2 façons. Reset Initial détruit tout l'environnement (ce qui est habituellement plus d'un voudrait). Une autre façon est de masquer univers w/modules

Universe M R. Constraint M < R. 
Definition M := [email protected]{M}. Definition R := [email protected]{R}. 
Check M:R. Fail Check R:M. (*the hierarchy holds*) 

(*1. w/ modules:*) 
Module i. 
Universe M R. Constraint R < M. 
Check M:R. Fail Check R:M. (*still holds*) 
Definition M := [email protected]{M}. Definition R := [email protected]{R}. (*but now..*) 
Fail Check M:R. Check R:M. (*not any more*) 
Print Sorted Universes. (*2 Rs and Ms, w/ the old hierarchy masked by the new one*) 
End i. 

(*outside the module the old hierarchy holds*) 
Check M:R. Fail Check R:M. 

(*2. w/ Reset Initial:*) 
Reset Initial. Fail Check M:R. Fail Check R:M. 
Print Sorted Universes. (*the def-d univ-s are gone*)

Source

2017-04-08 19:35:06 jaam

Coq: libérer des univers

Répondre

Questions connexes