如何从 MMT 中的结构访问常量和符号？

Question

鉴于以下理论，为了小型 MWE 的目的将无意义的东西形式化，

theory Meta : http://cds.omdoc.org/urtheories?LF =
  ℕ: type ❙
  prop: type ❙
  or: prop ⟶ prop ⟶ prop ❘ # 1 ∨ 2 ❙
❚

theory S : ?Meta =
  c: ℕ ⟶ ℕ ⟶ prop ❘ # 1 + 2 ❙
  d: ℕ ⟶ ℕ ⟶ ℕ ⟶ prop ❘ # 1 |- 2 ∶ 3 ❙
❚

在声明了两个 S 结构后，如何访问 S 中的内容？

theory T : ?Meta =
  structure s1 : ?S = ❚
  structure s2 : ?S = ❚

  n: ℕ ❙

  // How do I access constants c, d and their notations from s1, s2?
❚

Answer 1

常量可通过 <structure name>/<constant name>

获得

theory T : ?Meta =
  structure s1 : ?S = ❚
  structure s2 : ?S = ❚

  n: ℕ ❙

  c_usage1 = s1/c n n ❙
  c_usage2 = s2/c n n ❙
  c_usage_combined = (s1/c n n) ∨ (s2/c n n) ❙

  d_usage1 = s1/d n n ❙
  d_usage2 = s2/d n n ❙
  d_usage_combined = (s1/d n n) ∨ (s2/d n n ) ❙
❚

符号在 第一个 表示标记

前添加 <structure name>/

例如，定义为# 1 + 2的表示法只有一个presentation marker+，因此通过... <structure name>/+ ...访问。 另一方面，定义为 # 1 |- 2 ∶ 3 的符号有两个表示标记：|- 和 ∶。通过 ... <structure name>/|- ... ∶ ...:

访问

theory T : ?Meta =
  structure s1 : ?S = ❚
  structure s2 : ?S = ❚

  n: ℕ ❙

  c_usage1 = n s1/+ n ❙
  c_usage2 = n s2/+ n ❙
  c_usage_combined = (n s1/+ n) ∨ (n s2/+ n) ❙

  d_usage1 = n s1/|- n ∶ n ❙
  d_usage2 = n s2/|- n ∶ n ❙
  d_usage_combined = (n s1/|- n ∶ n) ∨ (n s2/|- n ∶ n) ❙
❚