问使用不相关的字段

EN

有没有可能在记录中声明不相关的字段，但仍然在其他地方使用它们？

假设我有

postulate f : ℕ → ℕ
record Silly x : Set where
  field
    n : ℕ
    s : f n ≡ x

open Silly

然后，我就可以

same-silly : ∀{x} {p q : Silly x} → f (n p) ≡ f(n q)
same-silly {x} {p} {q} = ≡-trans (s p) (≡-sym (s q))

但是如果我使用虚线字段，

record Silly x : Set where
  field
    n : ℕ
    .s : f n ≡ x  -- note the dot

那么same-silly就不能再被证明了-至少我不能证明。在上面的定义中，当我尝试使用s时，Agda会通知我Identifier s is declared irrelevant, so it cannot be used here。

我知道我通过点缀s来声明它无关紧要，但我仍然想要一点访问权限:有足够的权限来定义same-silly。有没有办法获得这一小部分而不是完全访问权限？我的意思是，我认为s是一个连贯性条件，我想在蓝月亮上使用一次，但不是很重要，所以点。也许可以忽略这一段。

有没有可能形成same-silly并对s进行打点？

(

旁白:虚线模式是否意味着命题相等与关系一致？

_~_ : ∀{x} (p q : Silly x) → Set
p ~ q = n p ≡ n q

？特别是，通过添加到记录constructor _#_中，我可以显示

eq : ∀{m x}{p q : f m ≡ x} → (m # p) ≡ (m # q) 
eq = ≡-refl

但我还不能确定点划域是否意味着绝对相等会忽略点划线域。

我正在浏览http://wiki.portal.chalmers.se/agda/agda.php?n=ForkedReferenceManual.Records#Irrelevantfields；它说有虚线字段的投影，但似乎我不能在任何地方使用它们。

)

如有任何帮助，我们不胜感激！