rev_rev_idとは、リストを2回逆順にすると元に戻る、というやつだ。
Leanで挑戦してみた。
Leanのインストール
バイナリがあるから、それを持ってくるだけ。
本格的にやりたい方は
https://righ1113.hatenablog.com/entry/2020/06/06/101151
をどうぞ。
開発環境
型の確認と、値の評価
#check
で型の確認ができる。#reduce
で値の評価ができる。
structured proofとtactic
まだやっていない。
Equational Reasoning
calc
でおこなうみたい。
Reasoningの中でrewrite(rw)できるのは大きいかも。
rev_rev_idの実装
例によってsnoc
を使う方法でやってみた。
みょんみょんさんの実装を参考にした。
.
.