2014-11-03から1日間の記事一覧
Coq の証明を書くときに,ただ tactics を一列に並べて書くと,まったく読めなかったり Coq のバージョンが上がって証明が通らなくなったときにどこでこけてるのかわからなくなったりして不都合なので,証明の構造を proof script のテキスト上にも反映させ…
Coq の証明を書くときに,ただ tactics を一列に並べて書くと,まったく読めなかったり Coq のバージョンが上がって証明が通らなくなったときにどこでこけてるのかわからなくなったりして不都合なので,証明の構造を proof script のテキスト上にも反映させ…