懸而未決METAS在阿格達

Question

限定記錄時

考慮下面的代碼：

module UnresolvedMeta where 

    record Test (M : Set) : Set1 where 
    field 
     _≈_ : M -> M -> Set 
     _⊕_ : M -> M -> M 
     assoc⊕ : ∀ {r s t} -> ((r ⊕ s) ⊕ t) ≈ (r ⊕ (s ⊕ t)) 

    data ℕ : Set where 
    n0 : ℕ 
    suc : ℕ -> ℕ 

    data _==_ : ℕ -> ℕ -> Set where 
    refl== : ∀ {k} -> k == k 

    _+_ : ℕ -> ℕ -> ℕ 
    k + n0 = k 
    k + suc m = suc (k + m) 

    lem-suc== : ∀ {k m} -> k == m -> suc k == suc m 
    lem-suc== refl== = refl== 

    assoc+ : ∀ {i j k} -> ((i + j) + k) == (i + (j + k)) 
    assoc+ {i} {j} {n0} = refl== {i + j} 
    assoc+ {i} {j} {suc k} = lem-suc== (assoc+ {i} {j} {k}) 

    thm-ℕ-is-a-test : Test ℕ 
    thm-ℕ-is-a-test = record { 
    _⊕_ = _+_; 
    _≈_ = _==_; 
    assoc⊕ = assoc+ 
    } 

當裝載有阿格達（版本2.3.2.2），阿格達打印「在以下位置未解METAS」有關行的錯誤倒數第二行：

assoc⊕ = assoc+ 

並特別指向assoc +。

如何提供提示或以其他方式更改代碼，以便在沒有此警告的情況下進行編譯？

我當然可以通過取消隱藏參數擺脫它，但是這意味着我將不得不處處指定明確的論點，即使在不需要它的地方......

Answer 1

您可以利用以下事實： Agda允許您在lambda抽象中指定隱式參數。更具體地講，你可以這樣寫：

λ {r s t} → assoc+ {r} {s} {t} 
-- with a type {r s t : ℕ} → ((r + s) + t) == (r + (s + t)) 

事實上，上面的表達，使編譯器高興更換assoc+。這似乎是統一與最後一個參數（t）一個問題，所以我們甚至可以忽略r和s，僅在t填寫明確：

assoc⊕ = λ {_ _ t} → assoc+ {k = t}