読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

fold_leftとfold_rightが同じになるとき

fold_leftとfold_rightの結果が同じになるときが気になったので少し調べてみた。例えば文字列のリストを連結して一つの文字列を生成する次の例はfold_leftでもfold_rightでも同様に定義できて同じ関数になる。Coqで書くと次のような感じ。 Definition xs := …