agda

2熱度

1回答

我從「Agda的殘酷介紹」中獲取此信息http://oxij.org/note/BrutalDepTypes/ 假設我們想要在偶數上定義除以二的數。我們可以做到這一點爲： div : (n : N) -> even n -> N div zero p = zero div (succ (succ n)) p= succ (div n p) div (succ zero)() N是自然數，

0熱度

1回答

類型檢查的實例含義

我正在學習如何在Agda中實現「類型類」。作爲一個例子，我試圖實現羅馬數字，其組成與＃將進行類型檢查。我不明白爲什麼阿格達抱怨沒有實例加入（羅馬_ _）（_羅馬_）_ - 顯然，它可能不知道是什麼的自然數代替那裏。有沒有更好的方式來介紹羅馬數字，沒有「構造函數」形式？我有一個構造函數「madeup」，它可能需要是私有的，以確保我只有「可信」的方式通過Join來構建其他羅馬數字。 module

2熱度

1回答

Agda函數，函數匹配類型

我想創建一個輔助函數，它將從索引或參數化類型中取出一個詞並返回該類型參數。 showLen : {len : ℕ} {A : Set} -> Vec A len -> ℕ showLen ? = len showType : {len : ℕ} {A : Set} -> Vec A len -> Set showType ? = A 這可能嗎？（？我可以看到showType []可能

4熱度

2回答

使用計算函數的值在AGDA

我仍然在試圖總結我的周圍AGDA頭，所以我寫了一個小井字棋遊戲類型證明 data Game : Player -> Vec Square 9 -> Set where start : Game x (- ∷ - ∷ - ∷ - ∷ - ∷ - ∷ - ∷ - ∷ - ∷ []) xturn : {gs : Vec Square 9} -> (n : ℕ) -

1熱度

1回答

agda中的雙重否定插入

我想要澄清agda中的雙重否定。即使 z≡z : 0 ≡ 0 z≡z = refl 我無法弄清楚如何證明： ¬¬z≡z : (0 ≡ 0 → ⊥) → ⊥ ¬¬z≡z ? 這是長手¬ (0 ≢ 0)。也許我錯過了一路上某處agda的成語。理想情況下，我想用最少的參考來解釋標準庫。

4熱度

1回答

\ forall（∀）在簽名中究竟意味着什麼？

從我收集的關於agda的信息中我可以得出結論∀ {A}相當於{A : Set}。現在我注意到， flip : ∀ {A B C} -> (A -> B -> C) -> (B -> A -> C) 是無效的（一些關於設置\歐米茄這又似乎是一些內部的東西，但 flip : {A B C : Set} -> (A -> B -> C) -> (B -> A -> C) 是罰款。任何人都可以清除

5熱度

1回答

使用依賴對在Agda中的問題

我在學習Agda by tutorial，現在我正在閱讀有關從屬對。所以，這是代碼的片段： data Σ (A : Set) (B : A → Set) : Set where _,_ : (a : A) → (b : B a) → Σ A B infixr 4 _,_ Σprojₗ : {A : Set}{B : A → Set} → Σ A B → A Σprojₗ (a

4熱度

1回答

trustMe有多危險？

這裏是我瞭解Relation.Binary.PropositionalEquality.TrustMe.trustMe：它似乎採取任意x和y，並且：如果x和y是真正平等的，它成爲refl 如果他們不，它像postulate lie : x ≡ y 。現在，在後一種情況下，它可以很容易地阿格達不一致，但是這本身是沒有這麼多的問題：它只是意味着使用trustMe任何證明是訴諸權威證明。此外，儘管你

6熱度

1回答

終止檢查合併

阿格達2.3.2.1無法看到下面的函數終止： open import Data.Nat open import Data.List open import Relation.Nullary merge : List ℕ → List ℕ → List ℕ merge (x ∷ xs) (y ∷ ys) with x ≤? y ... | yes p = x ∷ merge xs (y

1熱度

1回答

在阿格達

啓用尾調用優化我使用Emacs與agda-mode，並寫了這個功能： pow : Nat → Nat → Nat pow m n = pow' 1 m n where pow' : Nat → Nat → Nat → Nat pow' acc _ zero = acc pow' acc m (succ n) = pow' (m * acc)