前回: キャスト - kururu_goedel’s diary 文字列変換 特に命題が複雑になってきたときには、(Leanの)変数に格納されている論理式を表示してチェックしたい。そのような機構はMathlib.ModelTheoryにはない。本格的に公理化された集合論のモデルをやり始める前…