| 3.21 |
| Title |
Domain (includes arguments with proper class values) #DefBigDomain #label-domain-includes-arguments-with-proper-class-values |
| Classification |
Definition |
| Formula |
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{F} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/dom-op.html}{\mathrm{Dom}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{F} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/exists-binder.html}{\exists} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{b} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{b} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{F} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
CpDom |
| Scheme of Types |
0(∀([F@Variable]:[Class@Type])(Dom([F@Class.Expression])={[x@Class.Expression]|∃([b@Variable]:[Class@Type])(([x@Class.Expression],[b@Class.Expression])∈[F@Class.Expression])})) |
| Verification |
Definitional (Kernel AST) · Standalone Entry (DefBigDomain) → · (3.21) · #DefBigDomain |
|