全称変数は、型宣言された変数で、その型の任意のモノを表す。任意変数と言ってもいい。$`\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\for}{\Keyword{for } }
\newcommand{\assume}{\Keyword{assume } }
\newcommand{\consider}{\Keyword{consider } }
\newcommand{\st}{\Keyword{ st } }
\newcommand{\endBlock}{\Keyword{end } }
`$
$`\for x : X`$
または、
$`\assume x : X\\
\quad \cdots\\
\endBlock
`$
で全称変数が導入される。$`\for`$で導入された変数のスコープはすぐ外のブロックの終了まで。$`\assume`$は自分のブロックを作る。
それに対して特称変数は条件と共に導入される。
$`\consider x : X \st P(x)\\
\quad \cdots\\
\endBlock
`$
全称変数／特称変数は、ブロックに閉じ込められたスコープ付き変数〈scoped variable〉で、スコープ外に漏れることはない。外のスコープの名前をシャドーするが、通常はシャドーしないように使う。
全称変数は、対応する全称束縛変数に閉じ込めてスコープからoutgoingできる。逆に、存在束縛変数は、特称変数としてスコープ内にincommingできる。
全称変数は、スコープ内で自由変数として使ってよく、特称変数は条件を満たす定数のように使ってよい。
- Lean 4で、全称変数の生成は、variable宣言、関数引数、assume〈ラムダ変数〉で行う。
- Lean 4で、特称変数のサポートがほとんど無いようだ。これがネックになっている。
