CoqでModuleをまるごと仮定するVariableみたいなの
結論: Declare Module を使うと良い。
-
yoshihiro503
- 1255
- 0
- 0
- 0
-
- いいね！0
Yoshihiro Imai
@yoshihiro503
有限集合 MSetsは具体的にListから作ろうとすると set A のAの部分の型についてDecidableだったり比較可能だったりが成り立たないと使えないっぽい。めんどくせー。 #Coq
2015-08-10 14:38:05
Yoshihiro Imai
@yoshihiro503
@chiguri Variableみたいに、 Module Variable M <: MT. みたいに書きたいんです。 #coq
2015-08-10 14:44:30
Yoshihiro Imai
@yoshihiro503
@chiguri Functorだと(M:Sig)を使うところ全部をFunctorにしなきゃいけなくなるじゃないですかー。
2015-08-10 14:47:57
Sosuke MORIGUCHI
@chiguri
@yoshihiro503 Declare Moduleというコマンドですかね（そこまで使ったことがなかったので）
2015-08-10 14:54:31
Yoshihiro Imai
@yoshihiro503
@chiguri ありがとうございます！私が欲しかったのはこれでした！ #Coq #Module #ModuleType #DeclareModule
2015-08-10 14:58:21
Yoshihiro Imai
@yoshihiro503
実態を気にせずにMSetInterface.Setsなどを仮定するときに便利かも。 / “Sosuke MORIGUCHIさんはTwitt…” htn.to/bDGjwN #Coq #Module_System #Deculare_Module #Functor
2015-08-10 15:26:30