問題タブ [idris]

構文と Haskell との違いに慣れるために、Idris で基本的なモナド パーサーを作成しています。私はそれがうまく機能する基本を持っていますが、パーサー用の VerifiedSemigroup と VerifiedMonoid インスタンスを作成しようとして立ち往生しています。

これ以上苦労することなく、パーサー タイプ、Semigroup、および Monoid インスタンス、および VerifiedSemigroup インスタンスの開始を次に示します。

私は基本的に の後intros、次の証明者の状態で立ち往生しています:

rewriteどうにか一緒に使えそうな気がするappendAssociativeのですが、 lambda の「中に入る」方法がわかりません\s。

とにかく、私は演習の定理証明の部分で立ち往生しています - イドリス中心の定理証明のドキュメントをあまり見つけられないようです。おそらく、Agda のチュートリアルを見始める必要があると思います (ただし、Idris は、私が学びたいと確信している依存型型言語です!)。

私は次のコードを持っています (ほとんどの場合、emacs で idris-mode を使用して自動生成されます):

ファイルを REPL (Cc Cl) にロードしようとすると、次のエラー メッセージが表示されます。

私は何か間違ったことをしていると思いますが、何がわかりません。

最初に cabal の更新/アップグレード プロセスを実行するので、cabal-install-1.20.0.3 を取得します。それから私は：

私は得る：

（それが問題になる場合は、OS X 10.9.4を実行しています）

私はemacsを初めて使用し（idris-vimを機能させることができないvimから来ました）、これらのパッケージをel-get経由でインストールしました：

私の ~/.emacs.d/init.el は次のようになります:

私は悪を使用しており、idris-mode には悪で動作するバインディングがあるため、vimのケース分割の例に従ってみました。新しいセッションから開始すると、次のことが起こります。

1. vadd.idr ファイルを開きます。このファイルには、既に 3 行 (うち 1 行は空白) が含まれています。
2. 最後の行に移動して を押し\dます。
3. 長いエラー メッセージが表示されますが、読む前に消えてしまいます。
4. Idris REPL が新しい分割ペインで開きます。
5. コマンド ライン (ウィンドウの下部) に が表示されますBuffer vadd.idr has no process。また、挿入モードで入力して、REPL を試します。Enter キーを押すと、 が表示Buffer *idris-repl* has no processされ、それ以上何も起こりません。

Linux シェルでは、echo $PATHが生成され、期待どおりにシェルから動作します。/home/james/bin /home/james/.cabal/bin /home/james/bin /usr/local/sbin /usr/local/bin /usr/bin /usr/bin/vendor_perl /usr/bin/core_perlidris

(数秒間) emacs を終了するZZと、アクティブなプロセスが存在すると言われます。ここに私が示しているプロセスリストがあります：

接続されている可能性があるため、idris-vim を使用して vim の同じファイルから取得したエラーは次のとおりです。

リーダーバインディングが機能しないため、 ex コマンドを使用します (まだ別の問題があります)。

このような長い質問をして申し訳ありません。関係のない情報を追加することになるとしても、最も関連性の高い情報を含めたかったのです。

編集：もっと; デバッガーを見つけました (メニューから「エラー時にデバッガーに入る」を設定します)。

を押す\dと、バッファに次のように表示されます。

そしてexコマンドラインで

何をしようとしているのかわからない。

編集: vadd.idr のバッファーのステータス行の右端は次のとおりです (正しい用語?):

Not loaded心配そうに見えますが、それ以上のことはわかりません。

編集：Vimの問題に戻り、実行しました

ログからのすべては、最後までかなり正常に見えます (エラーによって引き起こされます):

そのため、ログファイルに含まれていることがわかりました

これらのシェル コマンドをシェルから実行すると、次のようになります。

ちなみに、プレーンidris vaddr.idrは問題なく動作します。

現在、 経由で Idris をビルドしていcabal install idrisます。出力への応答:

でビルドを追跡することにしましたtail -f /home/me/.cabal/logs/idris-0.9.14.3.log。

出力の大部分は意味がありますが、次の行に沿っています。

のみを含む多くの行があります

*** CPSZ:

それで、純粋に好奇心から、「 」が何*** CPSZ:を表しているのか疑問に思っていました。

関数内で暗黙の変数を使用するにはどうすればよいですか? 最も単純なケースに還元すると、次のことが可能になります。

エラーを取得せずに:

内部から値にアクセスする方法はありますか? nそれとも中を求めるのと同じsin nですか？

Vectこの場合、それが「全単射」であることを証明し、そこから変数を復元することは可能ですか?