CoqのReset（より一般的には、無料）ユニバースへの道はありますか？Coq：空きユニバース
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*)
私は何でも、M = Type.2です。私はCoqにいる8.5
私は2つの方法を見つけました。 Reset Initialは環境全体を破壊します（通常は複数の環境が必要です）。もう一つの方法は、私はそこに可能であるかを知るために8.5コードベースに慣れていないよ怖いモジュール
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*)
/wのユニバースをマスクすることで、8.6はそうYMMVをチェックし、宇宙の新しい実装を持っています。 – ejgallego
@ejgallego： 'Universe M. Reset M.'は8.6で宇宙をクリアしますか？ – jaam
わかりませんが、「自動生成定数ではリセットが実装されていません」という警告が出力されます。 – ejgallego