1.
テンプレート
2.
Proof handling
2.1.
Search
3.
Tactics
3.1.
apply - 適用
3.2.
case - 条件分岐
3.3.
congruence - 合同
3.4.
discriminate - 構築子の区別
3.5.
injection - 単射性
3.6.
inversion - 単射の逆
3.7.
simpl - 簡略化
4.
Use Case
4.1.
仮定と前件の移動
4.2.
選言の分解
4.3.
同値 iff の分解
4.4.
補題の導入
4.5.
= と == の言い換え
4.6.
存在量化子
Light (default)
Rust
Coal
Navy
Ayu
Coq/SSReflect/MathComp
Search