Imports

A module can import other modules. In the importing module, elements declared in the imported module can be used.

There are three kinds of import declarations: protecting, extending and using (or just pr, ex and us):

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

The name of a module to be imported is written in <module-exp>.

Each of pr, ex and us states to what extent the intended models of the imported modules are preserved within those of the importing modules.

When importing NAT+ with ex, A new element nan can be added to Nat, however it is not allowed when the import mode is pr:

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

When importing NAT+ with us, Terms s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) (=12) and 0 are allowed to be a same element. Then, a specification of arithmetic modulo 12 is obtained (*). This is not allowed when importing modules with pr or ex.

(*) In HOUR12, it holds that not only 12 = 0 but also 13 = 1, 14 = 2, and so on.

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

Original Copyright © Takahiro Seino, all rights reserved.