ほんとうはこわいIdris 〜 tacticメタプログラミング - Qiita

はじめに Idris分からん! 誰か教えてくれー こわくないIdris Idrisについて全く知らないって人は、僕が以前書いた記事を読んでください。 こわくない Idris で M59のブログ を検索 tacticとは カリー゠ハワード同型対応があるからプログラムを書くことがそのまま証明を書くことになるのだが、それとは別に定理証明器のとるべき戦略=tacticを記述することによっても証明を書くことができる。 Coqのtacticと比べるとIdrisのそれはとても貧弱に見える。前試したときは、自分でプログラム書いて証明した方がまだ楽なんじゃないかと思った。 Language.Reflectionモジュールを使うと、tacticを生成する関数を定義できる。例えば、Data.Vectモジュールに定義されているfindElemがある。 Elem その前に、Elemというデータ型について書いておこう

[minamiyama1994]

「型推論時実行」なにそれヤバイ

[zyzy]

Idrisを触って「型周りの書き方が整理されたHaskell」くらいにしか理解できていないので、この辺いずれちゃんと理解したいんだけど、Idrisをしっかり追いかけるのが正しいのか、まずCoqをやるべきなのか……。