idris

2熱

1答えて

どのように定義できますか？私はその文書に関するこの問題に関する情報は見つけていない。リストとベクトルについてのみ。 contribパッケージで

2熱

1答えて

私はIdris v.1.0をインストールし、サンプルコードをRosetta CodeのProof sectionから少しずつ実行しました。すべてがうまくいき、次のフラグメントになります。'class'キーワードは推奨されていません。代わりに 'インターフェース'を使用してください。エラー。 -- 3.1, Prove that the addition of any two even number

0熱

1答えて

CabalでIdris v 1.0にアップグレードしますか？

は考える：私は盲目的に、この出力を参照するcabal install idrisを実行して、アップグレードしようとした私は、バージョン1にアップグレードしたい $idris -v 0.99 はしかし、：だから $cabal install idris Resolving dependencies... All the requested packages are already inst

1熱

1答えて

この機能がREPLをハングアップするのはなぜですか？

Test-Driven Development with Idrisの第9章には、以下のデータタイプとremoveElem機能があります。 import Data.Vect data MyElem : a -> Vect k a -> Type where MyHere : MyElem x (x :: xs) MyThere : (later : MyElem x xs)

4熱

1答えて

なぜ "mod"に関連する等価性がIdrisでタイプチェックでないのですか？

はなぜ以下です。TypeCheckます： v1 : mod 3 2 = 1 v1 = Refl しかし、これは罰金です。TypeCheckます： v2 : 3 - 2 = 1 v2 = Refl

1熱

2答えて

Infの値が自動的に

パターンマッチング後に強制されるのは、我々は無限のリストがあるとしましょう： data InfList : Type -> Type where (::) : (value : elem) -> Inf (InfList elem) -> InfList elem をそして、我々はその有限個の要素がしたい：残っているもの、だから、 getPrefix : (count : Nat)

2熱

1答えて

Idrisではx == y = p（x）== p（y）という一般的な概念を定義できますか？

ドメインタイプt2に、pというドメインタイプを投影して、タイプラッパーを使用してドメインタイプt1に同等性を定義するというコンセプトを具現化するタイプコンストラクターを定義します。次具体例t1 = ABC、= Natt2とpが機能abc_2_natここで、動作します： %default total data ABC = A | B | C abc_2_nat : ABC -> Nat

4熱

1答えて

Idrisインタラクティブでこの再帰関数をどのように評価するのですか？

Idrisにダブリング、私はthis Haskell functionをIdrisに移植しようとしていました。私はインタラクティブイドリスでそれを呼び出すとき windowl : Nat -> List a -> List (List a) windowl size = loop where loop xs = case List.splitAt size xs of

1熱

1答えて

Idrisには同等のハッカーや追跡がありますか？

つまり、Idrisに書かれたオープンソースソフトウェアの中央パッケージレポジトリはまだ存在しますか？何人かのグーグルが私をidris-hackers githubページhereに導いてくれました。もちろん、Idrisで書かれたgithubでプロジェクトを検索することもできます。私は基本的にIdrisのパッケージを探すために紛失している別のよく知られているサイトがあるかどうか疑問に思っていました。