Naming convention for formalized proofs

[iehality]

提案：HilbertStyle 下の証明名は

1. 命名が混乱している（たとえば or₃'''! のような名前は読みやすくはない）
2. メタ論理の論理結合子名と形式化された論理結合子名が混合していてわかりにくい．

などの問題がある．次のような Łukasiewicz 風の記法で一貫した命名基準を試す．

Naming Convention

The names of the formalized proofs are determined by the following steps. (e.g. 𝓢 ⊢! (φ ⋏ ψ ➝ χ) ⭤ (φ ➝ ψ ➝ χ)):

1. Convert the formula to Łukasiewicz's notation (ECKφψχCφCψχ).
2. Remove meta variables (ECKCC).
3. Make it lowerCamelCase (eCKCC).
4. Postfix ! if it is a proposition (eCKCC!).

[SnO2WMaN]

1. Naming Conventionの3の最初の文字のlowercaseにするのは要らないような気もする．（ここだけLeanの慣習的な命名規則に沿わないことになるが，そもそも記号列なのでここまで合わせる必要は無い気もする）
2. 適当に#evalで名前を出力してくれるツールがあるとミスが無くリネームできて良さそう．