リフレクションのしくみをつくる - Qiita2015/08/11 2015/08/16 2015/09/12 「スモール SSReflect の製作」から改題 @suharahiromichi はじめに 命題(Prop型)をbool型の式に変換すること（とその逆）をリフレクションと呼びます。 例： x = y と x == y 命題をbool型の計算に変換することで、命題の証明が簡単になる場合があります。そのリフレクションを「狭い範囲」で行い、証明の効率化を図るのが、CoqのSmall Scale Reflection (SSReflect) 拡張です。 今回は、SSReflectのしくみを理解することを目的に、Starndard Coqで「SSReflectもどき」を作り、Leibniz同値関係とbool値等式のリフレクションができるまでを示します。 それを通して、Coqのコアーション(coersion)や、カノニカル・ストラクチ
