Abstractors

The <#3926#>abstractor<#3926#> serves to denote values of an abstract type. It will often be used together with a <#3927#>display<#3927#>, to abstract from a composed realization to an abstract object.

(315,040)<#4642#> (000,030)<#4533#>abstractor<#4533#> 194 (000,010)<#4534#>(1,0)<#3929#>030<#3929#><#5492#>#tex2html_wrap7315#(060,010)<#5493#>type-name<#5493#><#5492#> (1,0)<#3932#>030<#3932#> <#5499#>(010,010)<#5502#>:<#5502#><#5499#> (010,010) (1,0)<#3935#>030<#3935#><#5504#>#tex2html_wrap7325#(100,010)<#5505#>compact-primary<#5505#><#5504#> (1,0)<#3938#>030<#3938#><#4534#> 195 <#4642#>

The part after the colon (a <#3939#>compact-primary<#3939#>) must have the type of the realization of the <#3940#>type-name<#3940#>.

(315,120)<#4643#> (000,110)<#4535#>compact-primary<#4535#> 196 (000,090)<#4536#>(1,0)<#3942#>070<#3942#><#5507#>#tex2html_wrap7341#(080,010)<#5508#>denoter<#5508#><#5507#> (1,0)<#3945#>070<#3945#><#4536#> 197 (025,080)<#3946#>(20,20)[lb]<#3946#> (025,070)<#4537#>(1,0)<#3947#>045<#3947#><#5510#>#tex2html_wrap7345#(080,010)<#5511#>object-name<#5511#><#5510#> (1,0)<#3950#>045<#3950#><#4537#> (195,080)<#3951#>(20,20)[rb]<#3951#> 198 (025,060)<#3952#>(20,20)[lb]<#3952#> (025,050)<#4538#>(1,0)<#3953#>045<#3953#><#5513#>#tex2html_wrap7349#(080,010)<#5514#>choice<#5514#><#5513#> (1,0)<#3956#>045<#3956#><#4538#> (195,060)<#3957#>(20,20)[rb]<#3957#> 199 (025,040)<#3958#>(20,20)[lb]<#3958#> (025,030)<#4539#>(1,0)<#3959#>045<#3959#><#5516#>#tex2html_wrap7353#(080,010)<#5517#>display<#5517#><#5516#> (1,0)<#3962#>045<#3962#><#4539#> (195,040)<#3963#>(20,20)[rb]<#3963#> 200 (025,020)<#3964#>(20,20)[lb]<#3964#> (025,010)<#4540#>(1,0)<#3965#>005<#3965#> <#5523#>(010,010)<#5526#>(<#5526#><#5523#> (010,010) (1,0)<#3968#>030<#3968#><#5528#>#tex2html_wrap7363#(080,010)<#5529#>expression<#5529#><#5528#> (1,0)<#3971#>030<#3971#> <#5535#>(010,010)<#5538#>)<#5538#><#5535#> (010,010) (1,0)<#3974#>005<#3974#><#4540#> (195,020)<#3975#>(20,20)[rb]<#3975#> 201 (005,080)<#3976#>(20,20)[rt]<#3976#> (015,080)<#4541#>(0,-1)<#3977#>060<#3977#><#4541#> 202 (205,020)<#4542#>(0,1)<#3978#>060<#3978#><#4542#> (215,080)<#3979#>(20,20)[lt]<#3979#> 203 <#4643#>

The value of an <#3980#>abstractor<#3980#> is the value of its <#3981#>compact-primary<#3981#>. The type of an <#3982#>abstractor<#3982#> is the type of the <#3983#>type-name<#3983#>, rather than its realization. Since the realization of a type is visible only in its defining packet, an <#3984#>abstractor<#3984#> with a specific <#3985#>type-name<#3985#> can only be used in the packet defining that <#3986#>type-name<#3986#>.