forked from EduCraft/curriculum-project-hub
sjfhsjfh
63416e06ea
- FeishuProfile 从 User.lean 移到 FeishuConnection.lean - User.lean 只留用户创建路径声明 - 清理所有 doc comment
33 lines
1017 B
Lean4
33 lines
1017 B
Lean4
import Spec.Prelude
|
|
|
|
/-!
|
|
# Feishu —— 组织飞书应用绑定与用户飞书信息
|
|
|
|
组织绑定一个飞书企业应用(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
|
|
|
|
/-- 用户的飞书信息(`PINNED`)。User 上的可选绑定载荷。 -/
|
|
structure FeishuProfile where
|
|
/-- 应用内身份(`OPEN`);调 API 的直接句柄,换应用即变。 -/
|
|
openId : I.FeishuOpenId
|
|
/-- 租户内身份(`OPEN`);换应用不变,比 open_id 稳定。 -/
|
|
userId : I.FeishuUserId
|
|
/-- 显示名(`OPEN`)。 -/
|
|
name : Option String
|
|
/-- 头像 URL(`OPEN`)。 -/
|
|
avatarUrl : Option String
|
|
|
|
end Spec.System
|