2015年8月21日

CoqでModuleをまるごと仮定するVariableみたいなの

結論: Declare Module を使うと良い。
Yoshihiro503 @yoshihiro503

有限集合 MSetsは具体的にListから作ろうとすると set A のAの部分の型についてDecidableだったり比較可能だったりが成り立たないと使えないっぽい。めんどくせー。 #Coq

2015-08-10 14:38:05
Yoshihiro503 @yoshihiro503

Moduleを仮定するVariableってできないんだろうか?Functorを使うしか無い?

2015-08-10 14:39:15
Sosuke MORIGUCHI @chiguri

Functorの取ってくるModuleの変数を使うっていう話だろうか・・・?

2015-08-10 14:43:13
Yoshihiro503 @yoshihiro503

@chiguri Variableみたいに、 Module Variable M <: MT. みたいに書きたいんです。 #coq

2015-08-10 14:44:30
Yoshihiro503 @yoshihiro503

@chiguri Functorだと(M:Sig)を使うところ全部をFunctorにしなきゃいけなくなるじゃないですかー。

2015-08-10 14:47:57
Sosuke MORIGUCHI @chiguri

@yoshihiro503 Declare Moduleというコマンドですかね(そこまで使ったことがなかったので)

2015-08-10 14:54:31
Yoshihiro503 @yoshihiro503

@chiguri ありがとうございます!私が欲しかったのはこれでした! #Coq #Module #ModuleType #DeclareModule

2015-08-10 14:58:21
Yoshihiro503 @yoshihiro503

chiguriさんはやはり最強のcoqerなのでは...

2015-08-10 14:59:13
Yoshihiro503 @yoshihiro503

実態を気にせずにMSetInterface.Setsなどを仮定するときに便利かも。 / “Sosuke MORIGUCHIさんはTwitt…” htn.to/bDGjwN #Coq #Module_System #Deculare_Module #Functor

2015-08-10 15:26:30

コメント

コメントがまだありません。感想を最初に伝えてみませんか?