ITADN

検証用のコマンドを自前定義している個所の見直しをする

#2380OpenSeasawher 创建于 2026-05-31
S
Seasawhercommented
# 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 条评论