forked from bai/curriculum-project-hub
sjfhsjfh
3ebe4b754d
Remove filler/redundant patterns: 钉死/钉, 本模块, likec4 画不出/画得出, 臆造, 散文, 分歧点测试, 纯 plumbing, 恰好, 留白, 宪法第N条, 刻意. No code definitions changed, only doc comments.
13 lines
276 B
Lean4
13 lines
276 B
Lean4
import Spec.Prelude
|
|
|
|
/-!
|
|
# User —— 用户创建路径
|
|
|
|
用户实体见 `Hierarchy.User`;外部连接见 `Spec.System.Connections`。
|
|
|
|
用户创建当前只定义管理员直接创建;飞书自助注册→管理员审批 `OPEN`。
|
|
-/
|
|
|
|
namespace Spec.System
|
|
end Spec.System
|