私は、バイナリと単項関数からツリーとして構築された、n-ary関数の従属型を定義しようとしています;これは(Vect n a) -> aの型と同型です） Idrisを学ぶ練習として。 n項関数に引数を適用する関数を定義しようとしている（（N-1）進機能を生成する）一方で、私は非常に疑わしいエラーを得た： Type mismatch between
ArityFn m a (Type
私は、ヒルベルト平面のジオメトリにインシデントの公理を実装しようとしています。 interface (Eq point) => Plane line point where
-- Abstract notion for saying three points lie on the same line.
colinear : point -> point -> point ->
私はIdrisを学んでおり、私はVectタイプのQuicksortを実装しようと考えていました。 しかし、ピボット要素とベクトルを指定すると、≤ピボット要素とピボット要素を持つ2つのベクトルを分割するユーティリティメソッドでは苦労しています。 splitListOn : Ord e => (pivot : e) -> List e -> (List e, List e)
splitListOn
thisのドキュメントには、replaceを使用して証明を完成させる方法が記載されていますが、rewriteが使用されています。これはreplaceという文章砂糖のようです。私はそれを明示的に使用する方法を理解することに興味があります。 私が正しく理解していれば、反射性によって証明可能となり、k = plus k 0という証拠与えられ、S (plus k 0) = S (plus k 0)としてS
idrisの従属レコードのタイプコンストラクタに対するパラメータにインタフェース制約を設定できますか？ 私はインターフェイスShow : Type -> Typeを持っていると言います。今、私は、次の依存のレコードに制約を配置する必要があります。 record Source s where
constructor MkSource
initial : s
私はそれが常にSh
のための式は、私が data MyType
= One
| Two
| Three
...
| Ten
のような列挙型を持っていると私はそれのためにEqインターフェイスを実装したいとします。私は次のようにそれをすることができました Eq MyType where
One == One = True
Two == Two =
次のスニペットのための（番組の）実装を（https://stackoverflow.com/a/37461290/2129302）から検索された： tensor : Vect n Nat -> Type -> Type
tensor [] a = a
tensor (m :: ms) a = Vect m (tensor ms a)
私は次のように定義したいと思います： mkStr :