検証用のコマンドを自前定義している個所の見直しをする
# Codex による調査ログ
LeanByExample 配下の全ファイルを見て、検証用として自前定義されているコマンド定義は以下でした。
- [x] LeanByExample/Lib/InSecond.lean:6
#in_second。渡したコマンドが 1 秒以内に終わることを検証。
- [x] LeanByExample/Diagnostic/Time.lean:45
#speed_test。実行時間が指定したミリ秒範囲内か検証。
- [x] LeanByExample/Type/MLList.lean:12
#speed_rank。1 つ目のコマンドが 2 つ目より指定倍率以上速いか検証。
- [x] LeanByExample/Type/Subtype/Pos.lean:6
#speed_rank。同名コマンドを別記事内で再定義。
- [ ] LeanByExample/Type/Async.lean:40
#speed_rank。同名コマンドを別記事内で再定義。
- [ ] LeanByExample/Diagnostic/GuardMsgs/ContainMsg.lean:7
#contain_msg。コマンド出力メッセージが期待文字列を含むか検証。
- [ ] LeanByExample/Diagnostic/Guard/GuardDiff.lean:26
#guard_diff。#guard 派生で、等式が false のとき左右の評価結果も出す検証コマンド。
- [ ] LeanByExample/Type/CommandElab/AssertType.lean:9
#assert_type。項が指定した型を持つか検証。
- [ ] LeanByExample/Diagnostic/Print.lean:106
#detect_classical。指定定理が Classical.* 系の公理に依存していないか検証。
補足: #guard, #guard_msgs, #check_failure は検証用コマンドとして多数使われていますが、このリポジトリ内で自作定義してい
るものではないので除外しました。#nano_time, #expand, #doc, #greet なども自作コマンドですが、検証用ではなく計測・表示・
説明用なので除外しています。
1 条评论