forked from bai/curriculum-project-hub
sjfhsjfh
38c3231190
- Connections/Prelude.lean: ConnectionProvider 枚举 (当前仅飞书) - Connections/Feishu.lean: FeishuAppBinding + FeishuProfile - Connections.lean: ConnectionBinding/ConnectionProfile inductive - Organization.feishu → connections: List ConnectionBinding - User.feishu → connections: List ConnectionProfile - 删除 FeishuConnection.lean
16 lines
396 B
Lean4
16 lines
396 B
Lean4
/-!
|
|
# Connections.Prelude —— 连接提供商
|
|
|
|
用户/组织的外部身份连接。当前仅 IdP 类别(飞书)。
|
|
模型 provider connection 是独立概念,见 `Spec.System.Organization`。
|
|
-/
|
|
|
|
namespace Spec.System
|
|
|
|
/-- 连接提供商(`PINNED`;当前仅飞书,未来可扩展钉钉/企微)。 -/
|
|
inductive ConnectionProvider where
|
|
/-- 飞书(`PINNED`)。 -/
|
|
| feishu
|
|
|
|
end Spec.System
|