名前でだまされない 続き

  • 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 のようにする。decl fun foo も使う。def struct Bar とか decl struct Bar : → Type とかも使う。

Lean では、だいたい def で済んでしまう。型と値の区别がないから。

def BinOp (α : Type) := α×α → α