寫構造爲功能阿格達

更好的辦法，我有寫構造爲功能阿格達

data List (X : Set) : Set where 
    <> : List X 
    _,_ : X -> List X -> List X

平等

data _==_ {l}{X : Set l}(x : X) : X -> Set l where 
    refl : x == x

和一致性的定義

cong : forall {k l}{X : Set k}{Y : Set l}(f : X -> Y){x y} -> x == y -> f x == f y 
cong f refl = refl

我試圖證明

列表

propFlatten2 : {X : Set } (xs0 : List X) (x : X) (xs1 : List X) (xs2 : List X) 
       -> (xs0 ++ x , xs1) ++ xs2 == xs0 ++ (x , xs1 ++ xs2) 
propFlatten2 <> x xs1 xs2 = refl 
propFlatten2 (x , xs0) x₁ xs1 xs2 = cong (λ l -> x , l) {!!}

有沒有更好的方式直接使用構造函數_,_而不是通過最後一行中的lambda？

來源

2014-11-23 nicolas

你可以做'_，_ x'，但是如果你需要''，''右邊的''X，恐怕你不得不使用lambda或類似'flip _ _ x'。 – Vitus 2014-11-24 00:28:47

有趣。如果你把它作爲答案，我可以將它標記爲這樣。 – nicolas 2014-11-24 09:30:05

難道你不是指'xs0 ++（x，<>）'而不是'xs0 ++ x'嗎？如果'xs1 ++ xs2'是，我不認爲後者是很好的類型。 – Cactus 2014-11-25 03:50:27

Agda對運算符的部分應用沒有任何特殊的語法。你可以，但是，使用該運營商在他們平時的前綴版本：

x + y = _+_ x y

這是非常方便，當你需要部分應用最左邊的參數（S）：當你需要爲部分應用參數

_+_ 1 = λ x → 1 + x

從右側開始，你的選擇更加有限。正如在評論中提到的，你可以使用（在Function找到）的便利功能，如flip之一：

flip f x y = f y x -- Type omitted for brevity.

然後的_+_簡單flip參數：

flip _+_ 1 = λ x → x + 1

有時你會發現運營商的唯一目的是使代碼更好一點。我能想到的最好的例子可能是Data.Product.,_。當您編寫從屬對（Data.Product.Σ）時，有時可以自動填寫該對的第一部分。而是寫：

_ , x

你可以這樣寫：

, x

很難寫一個專門的運營商，如上面的那個其實是值得的，到時再說;如果你唯一的用例是同時使用它，我會堅持使用lambda表達式，因爲它使得它非常清楚發生了什麼。

來源

2014-11-25 20:29:07 Vitus

寫構造爲功能阿格達

回答

相關問題