こんな感じかな。 theorem 定理の名前 require モジュール1, モジュール2 using 定義, 定理1, 定理2, 規則 for 宣言1, 宣言2 given 命題1, 命題2 holds 命題 proof 証明 end end考慮点は カンマの代わりにandか？ for given の繰り返しを許すか holdsの前にf…

まずやってみると： >>> lambda x, y: x + y at 0x0000000002B8ED68> >>> sumf = lambda x, y: x + y >>> sumf at 0x0000000002B8E668> >>> sumf(1, 2) 3 以下、どれも認めていいが、 λ(x, y). x + y λ(x, y).(x + y) λ x, y .(x + y) λ x, y :(x + y) lambd…