問題タブ [idris]

私はidrisとidris-vimから始めています。しかし\c (IdrisCaseSplit)、私がいる行を削除することがあります。私は次のプログラムで試します：

次に、カーソルを上に置いてvApp押す\dと、次のようになります。

最初のケースに移動しxsて押す\cと、次のようになります。

ここまでは順調ですがys、最初のケース ( vApp [] ys) に移動して を押す\cと、行全体が削除されます。

なぜ行が削除されたのですか？望ましい動作を得るにはどうすればよいですか (ys を [] に置き換えます)。

2 番目のケースで ys をケース分割しようとすると、同じことが起こりvApp (x :: xs) ysます。

• Mac OSX、VIM 7.4 で idris 0.9.14.3 を使用しています。
• 病原体で活性化されたidris-vim。
• idris-vim は動作しています (たとえば、\t は正常に動作します)。
• :map\cは、実際にマップされているものを返します:call IdrisCaseSplit()<CR>
• 干渉を避けるために、最小限のvimrcで試しました。

前もって感謝します。

注: idris 自体のバグのようですか?

なぜ Idris は、関数が定義の順序で表示され、 で宣言された相互再帰が必要なのmutualですか?

私は Idris が関数間の依存関係分析の最初のパスを実行し、それらを自動的に並べ替えることを期待しています。私は、Haskell がこれを行うと常に信じてきました。Idris でこれができないのはなぜですか?

Idris FFI で FPtr 型の NULL パラメーターを持つ関数を呼び出すにはどうすればよいですか? ライブラリを調べたところ、null ポインターも、整数をポインターにキャストする方法もないようです。

の住人でも、の住人でType 1もない人の例は? Idris REPL を調べている間、何も思いつきませんでした。TypeType

より正確には、次の結果が得られるものx以外を探しています。Type

(j : Nat) -> {auto p : So (j < n)} -> Fin na をに変換するタイプの Idris 関数を作成しようとしてNatいFin nます。ケースを機能させるZ(そして を出力する) ために、 の証明が を作成できるのに十分であることFZを証明しようとしています。しかし、私はこれを行う方法を理解できません。0 < nFZ : Fin n

Nat値を値に変換できる限りFin n(値が存在する場合)、まったく異なる関数を作成することにオープンです。Nat私の目標は、 anyを値に変換できる他の関数を用意しMod nて、たとえば に15 : Natマップすること3 : Mod 4です。私のModタイプには現在、単一のコンストラクターmkMod : Fin n -> Mod n.

たとえば、Idris の関数で型を返すことができます。

->しかし、タイプのリストを折り畳むために使用したい状況が発生しました（いくつかのパーサーを作成して実験したとき） 、つまり

だからそれtypeFold [String, Int]は与えるだろうString -> Int : Type. ただし、これはコンパイルされません。

しかし、これはうまくいきます：

を使用するためのより良い方法はあり->ますか?そうでない場合は、機能要求として提起する価値がありますか?

Idris で決定可能なパーサーと呼ばれるものを作ろうとしています。最初は自然数の解析だけを見ていましたが、予期しない問題に遭遇しました。それを生成するコードの最小限の例は次のとおりです。

これがコンパイルされることを期待しますが、代わりに

しかし、natToChar 0明らかに等しい'0'ので、ここで何が問題なのかわかりません。

アップデート

また、私がここでやろうとしていることにより直接的に関連する質問もしました。

この型を使用して、決定可能な解析を実行できる文字列について推論しています。

たとえば、数字 [0-9] を次のように定義します。

次に、次の関数を使用できます。

このs2n関数はコンパイル時に問題なく動作するようになりましたが、それ自体はあまり役に立ちません。Every Digit (unpack s)実行時にそれを使用するには、関数を使用する前に証明を構築する必要があります。

だから私は今、この関数のようなものを書きたいと思います:

それか、メンバーシップの証明または非メンバーシップの証明のいずれかを返したいのですが、これらのいずれかを一般的な方法で行う方法が完全にはわかりません。代わりに、Maybe文字だけのバージョンを試してみました:

しかし、その後、次の統合エラーが発生します。

しかし、タイプp ですChar -> Type。この統合の失敗の原因はわかりませんが、問題は以前の質問に関連している可能性があると思います。

これは私がやろうとしていることに対する賢明なアプローチですか? 現時点では少し多すぎるように感じますが、これらの関数のより一般的なバージョンが可能になるはずです。クラスがどのように機能するかと同様の方法で、キーワードを使用して aまたはautoを与える関数を記述できるとよいでしょう。Maybe proofEither proof proofThatItIsNotDecEq

私は、最近仕事で行ったことを (より簡単な方法で) 再構築することにより、Idris を学ぼうとしています。

貸方のベクトルと借方のベクトルを使用して総勘定元帳をモデル化するデータ型が必要です。私はここまで来ました：

しかし、既存の GL にレコードを追加する方法がわかりません。

のような関数で

新しい GL がルールに従っていることを確認/強制するにはどうすればよいですか?