2011-12-06から1日間の記事一覧
前回の発展のようなかんじで,GADT を用いて型レベル自然数同士の大小関係を表現する項を作れるようにし,「n が m より小さい」ことを示す項と Vec m a を受け取って n 番目の要素を返す関数を定義してみた. 例によって一度ランタイムに compare して LT, …
前回の発展のようなかんじで,GADT を用いて型レベル自然数同士の大小関係を表現する項を作れるようにし,「n が m より小さい」ことを示す項と Vec m a を受け取って n 番目の要素を返す関数を定義してみた. 例によって一度ランタイムに compare して LT, …