forked from bai/curriculum-project-hub
sjfhsjfh
c6b4d439ac
Info.lean 里把用户填写态误译成了"授权"(authorization),与 Permission 模块的 grant 概念撞车且语义错位。正确是 authoring surface = 撰写态:用户在 manifest 里 实际填写的形态(RawInfo/RawAuthor),归一化后即消失。仅措辞,无语义/类型改动。 lake build 绿。 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
14 lines
478 B
Lean4
14 lines
478 B
Lean4
import Spec.Courseware.Model.Primitives
|
|
import Spec.Courseware.Model.RichContent
|
|
import Spec.Courseware.Model.Element
|
|
import Spec.Courseware.Model.Lesson
|
|
import Spec.Courseware.Model.Info
|
|
|
|
/-!
|
|
# Courseware.Model —— 工程文件的内容模型
|
|
|
|
留白基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课
|
|
(`Lesson`)、课时元信息(`Info`:canonical author 为列表 vs `RawInfo` 撰写态)。
|
|
决策出处 ADR-0005 / 0006 / 0008。
|
|
-/
|