在使用其中導入綁定與

Question

以下阿格達代碼是非法的：

record F : Set where 
    field 
    A : Set 

a : (F : Set) → Set 
a f with A 
a f | x = x 
where open F f 

它是示出了用在where引入綁定可能是在with子句有用的人工例子。儘管是人爲的，但有一些更大的例子可能是可取的。

看來，爲什麼這是非法的原因是，with可能會導致參數由於統一而被更大的項取代。特別是早期的綁定可能在匹配with結果的子句中變得不可用。這是一個適用於任何解決方案的警告。

假設傳遞給with的表達式實際上足夠長以證明這種努力，是否有辦法模仿或緩解這種特性？

Answer 1

您可以使用let：

record F : Set₁ where 
    field A : Set 

a : F -> Set 
a f with let open F f in A 
a f | x = x 

對於嵌套with是你可以使用輔助功能：

record F : Set₁ where 
    field A : Set 

a : F -> Set 
a f = a' where 
    open F f 
    a' : Set 
    a' with A | A 
    a' | x | _ with A 
    a' | x | _ | _ = x 

不是很漂亮，但工程。