寻观「标准库」之书。
寻观「编译器核心」之「网页汇编核心」之「完整类型」之书。
寻观「编译器核心」之「网页汇编核心」之「类型作用域」之书。
寻观「编译器核心」之「网页汇编核心」之「类型身份」之书。
寻观「编译器核心」之「网页汇编核心」之「复合类型匹配」之书。
「：文言：先定作用域与身份，循父链验相容，乃验诸声明之体。汉语：组合递归组身份、显式继承链和复合类型方差，验证类型段；不代表指令或整个模块已经验证。：」
「网页类型上下文」即（「列」于「网页子型声明」）合（「列」于「网页类型身份」）也。
「网页取上下文型」乃化「网页类型上下文」而化「整数」而「网页子型声明」也。
「网页取上下文型」者会「境」而会「号」而虑「检」者「网页检查类型号」于（「长度」授以「网页子型声明」于（「境」中「零」））于「号」而「第N个」授以「网页子型声明」于「号」于（「境」中「零」）也。
「网页具体祖先相容」乃化「网页类型上下文」而化「整数」而化「整数」而「爻」也。
「网页具体祖先相容」者会「境」而会「源」而会「目」而
 虑「型」者「网页取上下文型」于「境」于「源」而虑「目标检」者「网页取上下文型」于「境」于「目」而
 若「网页身份同」于（「第N个」授以「网页类型身份」于「源」于（「境」中「一」））于（「第N个」授以「网页类型身份」于「目」于（「境」中「一」））则「阳」否则
 鉴（「型」中「一」）而有「罄」则「阴」或有（「列」【「父」】）则（虑「检」者「网页检查类型号」于「源」于「父」而「网页具体祖先相容」于「境」于「父」于「目」）或有「其他」则「发生事故」于『类型上下文父声明非法』也。
「网页具体抽象类」乃化「网页类型上下文」而化「整数」而「网页抽象堆型」也。
「网页具体抽象类」者会「境」而会「号」而鉴（（「网页取上下文型」于「境」于「号」）中「二」）而有「网页函数复合」于「签」则「网页函数堆」或有「网页结构复合」于「域」则「网页结构堆」或有「网页数组复合」于「域」则「网页数组堆」也。
「网页上下文堆相容」乃化「网页类型上下文」而化「网页堆型」而化「网页堆型」而「爻」也。
「网页上下文堆相容」者会「境」而会「源」而会「目」而鉴「源」而
 有「网页具体堆」于「源号」则（鉴「目」而有「网页具体堆」于「目号」则「网页具体祖先相容」于「境」于「源号」于「目号」或有「网页抽象堆」于「抽」则「网页抽象堆相容」于（「网页具体抽象类」于「境」于「源号」）于「抽」）
 或有「网页抽象堆」于「抽」则（鉴「目」而有「网页抽象堆」于「期」则「网页抽象堆相容」于「抽」于「期」或有「网页具体堆」于「号」则（虑「类」者「网页具体抽象类」于「境」于「号」而鉴「抽」而有「网页空函数堆」则「等于」于（「网页抽象堆序」于「类」）于「零」或有「网页空聚合堆」则「或者」于（「等于」于（「网页抽象堆序」于「类」）于「五」）于（「等于」于（「网页抽象堆序」于「类」）于「六」）或有「其他」则「阴」））也。
「网页验证类型段」乃化「网页共享型表」而化（「列」于「网页递归型组」）而（「网页共享型表」合「网页类型上下文」）也。
「网页验证类型段」者会「表」而会「组们」而
 虑「身份」者「网页建立类型身份」于「表」于「组们」而
 虑「诸型」者「串联」授以「网页子型声明」于「组们」而
 虑「境」者（「网页类型上下文」也「诸型」与（「身份」中「一」））而
 递归虑「逐型」其化（「列」于「网页子型声明」）而「有」者会「余」而鉴「余」而有「罄」则「元」或有「缀」于「型」于「尾」则（
 虑「检」者（鉴（「型」中「一」）而有「罄」则「元」或有（「列」【「父」】）则若「网页复合相容」于（会「甲」而会「乙」而「网页上下文堆相容」于「境」于「甲」于「乙」）于（「型」中「二」）于（（「网页取上下文型」于「境」于「父」）中「二」）则「元」否则「发生事故」于『子类型字段或函数签名不符合父类型』或有「其他」则「发生事故」于『多父类型非法』）而
 「逐型」于「尾」）
 而虑「检」者「逐型」于「诸型」而（「身份」中「零」）与「境」也。
