idris

2熱度

1回答

爲什麼Idris將Data.Vect的參數排序爲size然後是item-type？正如標題所說，

。在我熟悉的其他依賴系統（Agda和Coq）中，矢量類型定義爲Vect : Type -> Nat -> Type。把參數放在索引之前對我來說是有意義的，無論如何，它似乎是向量類型的標準。爲什麼伊德里斯使用Vect : Nat -> Type -> Type？

1熱度

2回答

Idris中的常量

在Idris中定義其他語言中常量的常用方法是什麼？這是嗎？ myConstant : String myConstant = "some_constant1" myConstant2 : Int myConstant2 = 123 如果是這樣，在REPL我聲明後，得到一個異常： (input):1:13: error: expected: "$",

2熱度

1回答

錯誤消息說'類'已棄用，源不包含'類'

我剛剛安裝了Idris v.1.0，並逐行運行Rosetta Code的Proof section示例代碼。一切工作正常，直到下面的片段，它產生'class'關鍵字已棄用。改用'interface'。錯誤。 -- 3.1, Prove that the addition of any two even numbers is even. evensPlus1 : {a : MyNat} -> {

2熱度

1回答

伊德里斯：試圖在總體檢查失敗重新實現fromInteger進行NAT

我有以下代碼： module Test data Nat' = S' Nat' | Z' Num Nat' where x * y = ?hole x + y = ?hole fromInteger x = if x < 1 then Z' else S' (fromInteger (x - 1)) 我得到最後一行一條錯誤消息： Test.id

1熱度

1回答

Idris：從標準庫隱藏數據類型，或者不導入標準庫

我知道有一種方法可以使用％hide隱藏導入庫中的函數。但它似乎不適用於數據類型名稱，如Nat和Vect。有沒有辦法隱藏數據類型名稱，或只是不導入標準庫？

4熱度

1回答

如何評估Idris交互中的遞歸函數？

涉足伊德里斯，我試圖將this Haskell function移植到伊德里斯。我覺得我成功了，有了這個代碼... windowl : Nat -> List a -> List (List a) windowl size = loop where loop xs = case List.splitAt size xs of (ys, []) => if leng

1熱度

1回答

伊德里斯有沒有相當於嘲弄或追求？

也就是說，是否還存在用Idris編寫的開源軟件的中央軟件包庫？一些谷歌搜索將我引向idris-hacker github頁面，here。當然，我也可以在伊德里斯編寫的github上搜索項目。我基本上想知道是否有另一個知名的網站我失蹤尋找伊德里斯包。

11熱度

1回答

在伊德里斯，我能證明自由定理，例如'forall t'類型的唯一（全部）函數。 t - > t`是`id`？

對於充分多態的類型，參數可以唯一地確定函數本身（詳見Wadler's Theorems for free!）。例如，類型爲forall t. t -> t的唯一總功能是標識功能id。是否有可能在伊德里斯陳述和證明這一點？（如果它不能在伊德里斯內部證明，它是真的嗎？）以下是我的嘗試（我知道函數的相等不是伊德里斯的原始概念，所以我斷言泛型的任何函數t -> t總是返回相同的結果作爲身份函數將返回

2熱度

1回答

什麼是Idris字典/地圖的類型

我該如何定義一個？我沒有在文檔中找到有關此事的任何信息。只關於List和Vector。

3熱度

1回答

在Idris中，「Eq a」是一種類型，我可以爲它提供一個值嗎？

以下example1是標準語法（如文檔所述），其中Eq a作爲約束條件。在example2中，我直接指定Eq a作爲參數的類型，編譯器接受它。但是我不清楚我可以指定哪種類型的值。對於特定類型a，例如Nat，我認爲以某種方式指定Eq Nat的實現是有意義的，或者是默認實現，或者是某個其他指定的實現。 %default total example1: Eq a => (x : a) -> (y :