forked from EduCraft/curriculum-project-hub
sjfhsjfh
39bd2c9ff7
- FeishuConnection.lean: FeishuAppBinding (appId + appSecretEnvelope) - Organization.feishu: Option FeishuAppBinding (Option 自带 1:1) - 删除 FeishuConnectionId (不再需要游离类型) - FeishuProfile 删除 connection 字段 (由 org 隐含)
22 lines
694 B
Lean4
22 lines
694 B
Lean4
import Spec.Prelude
|
|
|
|
/-!
|
|
# FeishuConnection —— 组织飞书应用绑定
|
|
|
|
一个组织绑定一个飞书企业应用(1:1, `Option` 结构自带)。用户经此应用登录、调飞书 API。
|
|
绑定是组织级的;用户通过所属组织隐含获得绑定作用域。
|
|
-/
|
|
|
|
namespace Spec.System
|
|
|
|
variable (I : Identifiers)
|
|
|
|
/-- 组织的飞书应用绑定(`PINNED`, 1:1)。一个组织至多绑一个飞书企业应用。 -/
|
|
structure FeishuAppBinding where
|
|
/-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
|
|
appId : I.FeishuAppId
|
|
/-- 飞书企业应用 app_secret 的信封引用(`PINNED`, ADR-0024;明文不入契约)。 -/
|
|
appSecretEnvelope : I.FeishuAppSecretRef
|
|
|
|
end Spec.System
|