「インスタンス」という言葉の使い方

[spinylobster]

訳は間違っていないと思いますが、日本語話者のLeanユーザが「インスタンス」という言葉を見ると咄嗟に「型クラスのインスタンス」のことだと解釈してしまって混乱が生じるかも知れないと思いました。 論理的結合子は帰納型の例である などの方が適切かも知れません。

https://github.com/aconite-ac/theorem_proving_in_lean4/blob/10e8be31ac8cbcea97dc2008dc4b48b9a86a4654/interacting_with_lean.md?plain=1#L545

原文

With the propositions as types correspondence, logical connectives are also instances of inductive types, and so we tend to use dot notation for them as well:

[aconite-ac]

ご指摘ありがとうございます。 確かに、この箇所ではLean上の用語「(型クラスの)インスタンス」と解釈されることを避ける訳語が適切だと思われます。 ご提案頂いた「論理的結合子は帰納型の例である」という表現に変更いたします。

また、この日本語訳全体で "instance" という英単語に対して「インスタンス」という訳語を当てている箇所が多数ありますが、そのそれぞれについて、型クラスと関係のない文脈では他の適切な訳語を当てることを検討いたします。