define（Scheme）, def（Lean）, 無し function（JavaScript）, func（Go言語、Swift）, fun（Standard ML）, fn（Rust, Zig）, proc（Nim）, sub（Perl） 無し（Ruby, Python, Lean） defun（Lisp） defstruct（Lisp） ここでは、def fun foo のようにする…

axiom, constant, parameter, hypothesis などは同義語であり、どれを選ぶかは好みの問題。 axiom exclusive_middle {P :Prop} : P∧￢P → False : Prop constant exclusive_middle {P :Prop} : P∧￢P → False : Prop parameter exclusive_middle {P :Prop} :…

e はルール（証明の名前＝定理の名前〉、利用側からはルール。Prover's English ＝ P-En OBTAIN ::= prove | show | present | reach | obtain RESULT ::= conclusion | target | result assume文 ::= {we}? assume x : X have文 ::= {we}? have x : X {from…

λ(x:Int, y:Int).(x*x + y :Int) を次にように書く。 assume x: Int, y: Int providing z: Int, return z + y of Int where z: Int := x*xもっと証明っぽく： we assume x: Int and y: Int it suffices to prove z: Int because the result comes from z + y…