idris

4熱度

1回答

這是我的問題。 Idris有一個累積的宇宙層次，宇宙由編譯器推斷。使用dosomethingreal : IO是否意味着層次結構中最低的宇宙？是IO : Type，從來沒有IO : Type 1？或者我可以在任何宇宙中進行IO操作？

2熱度

1回答

我最近一直在學習Idris，並決定嘗試編寫一個簡單的張量庫。我從定義類型開始。 data Tensor : Vect n Nat -> Type -> Type Scalar : a -> Tensor [] a Dimension : Vect n (Tensor d a) -> Tensor (n::d) a 正如你所看到的，類型Tensor由Nat的Vect A S描

2熱度

1回答

相關類型

前一段時間，我遇到了「獨特賣點」似乎是依賴類型的編程語言Idris。有人可以解釋什麼是從屬類型，他們正在處理什麼樣的問題？

2熱度

1回答

理解`K：納特** 5 * K = N`簽名

下面的函數編譯： onlyModByFive : (n : Nat) -> (k : Nat ** 5 * k = n) -> Nat onlyModByFive n k = 100 但到底是什麼k代表其Nat ** 5 * k = n語法？另外，我怎樣稱呼它？這是我的嘗試，但我不明白輸出。答案的 *Test> onlyModByFive 5 5 When checking an app

1熱度

1回答

確定是否總和平均分5？

Cactus演示瞭如何解決我的問題：Helper Function to Determine if Nat `mod` 5 == 0。他寫道： onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat onlyModBy5 n = n 於是，我試圖使用功能應用onlyModBy5到Vect n Nat的總和。 foo :

2熱度

1回答

伊德里斯：有界的算術雙

我是伊德里斯的新手。我需要創建一個描述有界數字的數據。所以我做了這樣的數據與這樣一個構造函數： data BoundedDouble : (a, b : Double) -> Type where MkBoundedDouble : (x : Double) -> {auto p : a <= x && x <= b = True} -> Bounde

0熱度

1回答

數據類型包含兩個和類型？

鑑於這些2和類型： data Foo = A Int | B String data Bar = C Int | D String 我想定義返回Either (Foo or Bar) String功能。所以，我試圖使： data Higher = Foo | Bar 但它無法編譯： *ADT> :r Type checking ./ADT.idr ADT.idr:3:6:Main.Fo

3熱度

1回答

在接口中約束函數參數

在使用函數的接口中約束函數參數的語法是什麼？我想： interface Num a => Color (f : a -> Type) where defs... 但它說，Name a is not bound in interface...

4熱度

1回答

與Idris接口的奇怪的錯誤消息

我想實現一個簡單的代數結構層次結構使用Idris接口。代碼如下： module AlgebraicStructures -- definition of some algebraic structures in terms of type classes %access public export Associative : {a : Type} -> (a -> a -> a) ->

5熱度

1回答

在伊德里斯與改寫策略苦苦掙扎

我正在通過Terry Tao的真實分析教科書，它從自然數中構建了基礎數學。通過儘可能多的證明形式，我希望熟悉Idris和依賴類型。我已經定義了以下數據類型： data GE: Nat -> Nat -> Type where Ge : (n: Nat) -> (m: Nat) -> GE n (n + m) 代表主張一個自然數大於或等於另一個。我目前正在努力證明這種關係的反思，即