| 3.24 |
| Title |
ifᵈₑₚ (dependent conditional over (Bool → Type)) #DefDependentConditional #label-if-dependent-conditional-over-bool-type |
| Classification |
Definition |
| Formula |
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/bool-sort.html}{\mathsf{Bool}} \href{../symbols/impl-conn.html}{\rightarrow} \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/conditionals-if-dep.html}{\mathsf{if}_{\mathsf{dep}}} \href{../symbols/typing-colon.html}{:} \href{../symbols/pi-binder.html}{\Pi} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{b} \href{../symbols/typing-colon.html}{:} \href{../symbols/bool-sort.html}{\mathsf{Bool}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/comma-delim.html}{,} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/variables.html}{T_e} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/top-const.html}{\top} \href{../symbols/delimiters-brackets.html}{)} \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/delimiters-brackets.html}{(} \href{../symbols/bot-const.html}{\bot} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/variables.html}{T_e} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{b} \href{../symbols/delimiters-brackets.html}{)} \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}{b} \href{../symbols/typing-colon.html}{:} \href{../symbols/bool-sort.html}{\mathsf{Bool}} \href{../symbols/delimiters-brackets.html}{)} \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/delimiters-brackets.html}{(} \href{../symbols/top-const.html}{\top} \href{../symbols/delimiters-brackets.html}{)} \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/delimiters-brackets.html}{(} \href{../symbols/bot-const.html}{\bot} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/conditionals-if-dep.html}{\mathsf{if}_{\mathsf{dep}}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{b} \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/typing-colon.html}{:} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/variables.html}{T_e} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{b} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/conditionals-if-dep.html}{\mathsf{if}_{\mathsf{dep}}} \href{../symbols/delimiters-brackets.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/conditionals-if-dep.html}{\mathsf{if}_{\mathsf{dep}}} \href{../symbols/delimiters-brackets.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}{)} \href{../symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
EIfDep |
| Scheme of Types |
0∀(Tₑ:Bool→Type), ((ifᵈₑₚ:Π(b:Bool),(⟦Tₑ(⊤)⟧→(⟦Tₑ(⊥)⟧→⟦Tₑ(b)⟧)))∧∀(b:Bool)∀(t₁:⟦Tₑ(⊤)⟧)∀(t₂:⟦Tₑ(⊥)⟧)((ifᵈₑₚ(b,t₁,t₂):⟦Tₑ(b)⟧)∧((ifᵈₑₚ(⊤,t₁,t₂)=t₁)∧(ifᵈₑₚ(⊥,t₁,t₂)=t₂)))) |
| Verification |
Definitional (Kernel AST) · Standalone Entry (DefDependentConditional) → · (3.24) · #DefDependentConditional |
|