leanified/CoreReader.lean

返回主张速览 · 声明与证明

哲学 0.2.1 · 已考虑的 Core 0.1.2。阅读视图来自本仓库公开的目标清单、读者稿和 Lean 文件；页面布局不改变其中的判定。

展开 Lean 与逐行解读 · 1 行

Lean逐行解读

L1import CoreReader.Engineering.Integration

导入 Engineering.Integration 及其传递依赖，使本工程的工程应用、继承接口、共同见证与不蕴涵证明可用；导入本身不陈述哲学定理。