Q&ACoqでは次のようにVariableコマンドを使って、実装せずに型だけ書いて実装を省略することができる。
Coq
1Variable user : Set. 2Variable name_of_user : user -> string.
しかし、Moduleでも同じことがしたい。例えば次のようなModule Typeがあったとする。
Coq
1Module Type UserSig. 2 Variable t : Set. 3 Variable to_name : t -> string. 4End UserSig.
このときUserSigを満たすUserモジュールがあったと仮定してコードを書きたい。でもファンクタだとモジュールの構造が一段深くなってお手軽じゃない気がする。Variableのようにお手軽に仮定したい。
回答1件
0
自己解決
Declare Module コマンドを使えばよいらしい: http://togetter.com/li/863526
投稿2015/08/21 10:31
編集2015/08/21 10:32
総合スコア7
あなたの回答
tips
プレビュー
バッドをするには、ログインかつ
こちらの条件を満たす必要があります。