| assertion | アサーション (プログラムのある部分で成立しているべき条件を指す場合) | |
| brace | 中カッコ | |
| (prove, show) by contradiction | 矛盾を導く証明 (Aから矛盾が導かれることから¬A を言う場合) | 背理法 × (これは正確には背理法ではない。背理法は¬Aから矛盾が導かれることによってAを言うものだが、これは二重否定の除去を含んでおり、直観主義論理の体系である Coq では一般には言うことができない。) |
| closure | 閉包 (数学的概念として出てきた場合) | クロージャ × |
| coercion | 強制型変換 | |
| Exercise | 練習問題 | 演習 × |
| Hoare triple(s) | Hoareの三つ組 | |
| optional | optional(訳さない)(練習問題の位置付けの場合) | |
| Proof Assistant | 証明支援器 | 証明アシスタント × |
| simplification | 簡約(coqの証明手法として出てきた場合) | 簡約化、シンプル化 × |
| n star(s) | (★をn個書く)(練習問題の難度の場合) | |
| tactic | タクティック | タクティク × |
| user | ユーザ | ユーザー × |
| (人名) | (カタカナにせずもとのまま残す。ただし boolean, cartesian, abelian など人名起源であっても変形されてしまっているものはこれに縛られない) |
(英語のアルファベット順に並べ直しました。(ummr)
