idris

3熱

1答えて

Idris判定結果のベクトル長

Idrisでは、述語に基づいて要素を削除したい場合、filter,dropWhile、takeWhileがあります。ただし、これらの関数はすべて、従属ペア(n : Nat ** Vect n elem)を返します。 Vectタイプとして返​​される関数はありますか？私は考えることができるものについては ： 変換後の長さのベクトルを示すタイプを実装Vect に依存ペアに変換Hereのように、（私はど

dependent-type idris 2017-10-02

---

3熱

1答えて

イドリス・リライトは

import Data.Vect import Data.Vect.Quantifiers sameKeys : Vect n (lbl, Type) -> Vect n (lbl, Type) -> Type sameKeys xs ys = All (uncurry (=)) (zip (map fst xs) (map fst ys)) g : {xs,ys : Vect n (

idris 2017-10-04

---

3熱

1答えて

イドリス -

このプログラムを考えてみましょ遅延評価の問題： module test import Effects import Effect.StdIO (>>==) : Maybe a -> Lazy (a -> Maybe b) -> Maybe b (>>==) Nothing (Delay map) = Nothing (>>==) (Just x) (Delay map) = map

monads lazy-evaluation idris 2017-10-19

---

2熱

2答えて

Idris - 2つの数値の等価性を証明する

2つの自然な引数をとり、それらの等価性の証明の多分を返す関数を書いてみたいと思います。 私は equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True) equal a b = case (a == b) of True => Just Refl False => Nothing にしようとしているが、私はこれを行うには

idris 2017-10-20

---

2熱

1答えて

暗黙的な引数の順序はどのようにidrisに影響しますか？

これは失敗します。 > the ({A : Type} -> A -> {B : Type} -> B -> (A, B)) MkPair (input):1:5:When checking argument value to function Prelude.Basics.the: Type mismatch between A -> B1 -> (A, B1) (

idris 2017-10-21

---

1熱

1答えて

難し私は次のように私の定義のデータ型の1つにプロパティを証明しようとしていますイドリス

で証明を適用する：：私はことを以前に証明事実を使用しようとしていますこれを証明しようとして reverseProof' : (inputBlock : Block iType iSize iInputs) -> (ind : Fin rSize) -> (rInputs : Vect rSize Ty) -> (receiveBlock : Block r

idris theorem-proving 2017-09-11

---

4熱

1答えて

イドリス誘導ステップ

上の証拠は、次の関数、私は次のエラーを取得するコンパイルしようとすると tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber) tryMove Z

idris 2017-10-06

---

0熱

1答えて

Idrisの証明のためにタイプシグネチャの用語を書き換えるには？

基本的には、再帰算術でn - mまたはm - nのいずれかがゼロに等しいことを証明したいと思います。これを達成するために、私は成功なしでrewrite ... in ...パターンを使用しようとしています。 以下は、基本コードである：最初の二つの穴 - + Main.hoyo1 [P] `-- m : Natural --------------------------------

idris proof-of-correctness 2017-09-11

---