Light
Rust
Coal
Navy
Ayu
Lean by Example
conv
conv
は変換モードに入るためのタクティクです。詳細については
Theorem Proving in Lean4
をご参照ください。