IF ๐ THEN A ELSE B FI \(\mathrm{IF}\;\psi\;\mathrm{THEN}\;A\;\mathrm{ELSE}\;B\;\mathrm{FI}\) — Class Conditional Functional Symbol (IF..THEN..ELSE..FI, AST Constructor: CpIf)
3-ary mixfix class conditional IF ๐ THEN A ELSE B FI defined by class comprehension (Entry DefClassConditional (3.22)). Clicking any of IF, THEN, ELSE, or FI navigates to this single symbol page.
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
IF ๐ THEN A ELSE B FI
\(\mathrm{IF}\;\psi\;\mathrm{THEN}\;A\;\mathrm{ELSE}\;B\;\mathrm{FI}\)
|
| Category | Functional Symbol (3-ary Mixfix Class Operator) |
| SML AST Constructor | HC (CpIf of ('Truth_EXP * 'Class_EXP * 'Class_EXP)) [in datatype Class_p, typetheory.ML:562] |
| Constructor Arguments | 1. Condition ๐ : Fm/Bool; 2. Then-class A : Class; 3. Else-class B : Class |
| Metatype / Signature | Bool/Fm ร Class ร Class โ Class |
| Binder Status | No โ 3-ary Mixfix Functional Symbol (All tokens IF, THEN, ELSE, FI link here) |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \mathrm{IF}\;\psi\;\mathrm{THEN}\;A\;\mathrm{ELSE}\;B\;\mathrm{FI} |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | โฆIF โฆ๐โง THEN A ELSE B FIโง = {โฆvโฆ | (โฆ๐โง โง (โฆvโฆโA)) โจ ((ยฌโฆ๐โง) โง (โฆvโฆโB))} |
| Related Symbols & Kernel Entries |