diff options
| author | Tanaka Akira | 2019-01-31 16:37:59 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 16:37:59 +0900 |
| commit | ad13db81f25f48d1a0c800b16200426003c08b07 (patch) | |
| tree | 8b2c5effd529e4ebc745168285a0f723cbc8ec95 /kernel/nativelambda.mli | |
| parent | 6c1c8f1d68ddb11b34411e85f3dc65229f9abe3c (diff) | |
\Sort is not a term.
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort" is changed to
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S" because
\Sort is not a term.
"S" is choosen to be consistent with the description of
Inductive Definitions.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions