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回答

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

    4熱度

    2回答

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

    1熱度

    1回答

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

    4熱度

    1回答

    從我收集的關於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 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回答

    這裏是我瞭解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)