輸入

あるモジュールで、別の定義済みモジュールの宣言を使用できるようにすることを、モジュールの輸入 (import) と呼ぶ。

モジュールの輸入には、protecting、extending、using (およびそれぞれの省略形 pr、ex、us) を用いる:

pr(<module-exp>)
ex(<module-exp>)
us(<module-exp>)

<module-exp> はモジュール式と呼ばれる式であり、輸入するモジュール名を指定する他、様々な指定が行える。最も簡単なモジュール式は、モジュール名である。より複雑なモジュール式については、本講義では割愛する。

pr、ex、us の違いは輸入する際に、元のモジュールが表すモデルにどのような変更を許容するかである。

例えば、ex では Nat に新しい要素 nan を追加することが許されるが、pr では許されない:

mod! NAT+NAN {
  ex(NAT+)
  op nan : -> Nat
}

また、us では s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) (12) と 0 を同じ要素と宣言することで、12 を法とする数を宣言できる※が、pr や ex では許されない

※ 12 = 0 だけでなく、13 = 1、14 = 2、... も一つの等式で宣言されていることに注意せよ。

mod! HOUR12 {
  us(NAT+)
  eq s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) = 0 .
}