DefSimpleConditional (3.23, Definition): simple_if (polymorphic non-dependent conditional over Type)

Standalone kernel entity record from 3. Set/Class-Theoretic Foundations (3.01–3.78) — View in Complete Entity Database (#DefSimpleConditional) →

Formula Display:

Proof Trees:

DefSimpleConditional (3.23) — simple_if (polymorphic non-dependent conditional over Type)

Morse-Kelley / Von Neumann-Bernays-Gödel class comprehension, sethood, ordinals, Dunaev pairs, cardinals, universes, and reflection.

Num Entity Database Record (Vertical Field Table)

Title	simple_if (polymorphic non-dependent conditional over Type) `#DefSimpleConditional` `#label-simple-if-polymorphic-non-dependent-conditional-over-type`
Classification	Definition
Formula	0∀(Tₑ:Type ), ((simple_if (⟦Tₑ⟧):Bool →(⟦Tₑ⟧→(⟦Tₑ⟧→⟦Tₑ⟧)))∧∀(t₁:⟦Tₑ⟧)∀(t₂:⟦Tₑ⟧)((simple_if (⟦Tₑ⟧,⊤,t₁,t₂)=t₁)∧(simple_if (⟦Tₑ⟧,⊥,t₁,t₂)=t₂))) 0\(\href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{T_e} \href{../symbols/typing-colon.html}{:} \href{../symbols/type-sort.html}{\mathsf{Type}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/comma-delim.html}{,} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/simple-if.html}{\mathsf{simple\_if}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/variables.html}{T_e} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/typing-colon.html}{:} \href{../symbols/bool-sort.html}{\mathsf{Bool}} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/variables.html}{T_e} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/variables.html}{T_e} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/variables.html}{T_e} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{t_1} \href{../symbols/typing-colon.html}{:} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/variables.html}{T_e} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{t_2} \href{../symbols/typing-colon.html}{:} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/variables.html}{T_e} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/simple-if.html}{\mathsf{simple\_if}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/variables.html}{T_e} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/comma-delim.html}{,} \href{../symbols/top-const.html}{\top} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{t_1} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{t_2} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{t_1} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/simple-if.html}{\mathsf{simple\_if}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/variables.html}{T_e} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/comma-delim.html}{,} \href{../symbols/bot-const.html}{\bot} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{t_1} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{t_2} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{t_2} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`EIf`
Scheme of Types	0`∀(Tₑ:Type), ((simple_if(⟦Tₑ⟧):Bool→(⟦Tₑ⟧→(⟦Tₑ⟧→⟦Tₑ⟧)))∧∀(t₁:⟦Tₑ⟧)∀(t₂:⟦Tₑ⟧)((simple_if(⟦Tₑ⟧,⊤,t₁,t₂)=t₁)∧(simple_if(⟦Tₑ⟧,⊥,t₁,t₂)=t₂)))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefSimpleConditional`) → · (3.23) · `#DefSimpleConditional`