咨询Lean4中`Implies`标识符不存在的原因

• Lean4里并没有移除Implies，而是直接用函数类型→来表达命题间的蕴含关系。因为Prop属于Sort类型层级，当a和b都是Prop时，a → b就对应逻辑上的“a蕴含b”。
• 对比你看到的And结构体：合取（∧）需要额外定义结构来封装两个命题的证明，所以Lean4用And结构体实现，附带intro构造器和left/right消除规则；但蕴含的本质和函数类型完全等价——证明a → b就是构造一个从a的证明到b的证明的函数，因此不需要单独定义Implies这个类型。
• 若要检查蕴含相关的类型，直接使用#check (→)或者针对具体命题（比如#check Nat → Prop）即可；→是Fun的语法糖，执行#check Fun也能看到它的定义。

示例代码：

#check (→)  -- 输出：Sort u_1 → Sort u_2 → Sort (max u_1 u_2)
#check Fun  -- 输出：Sort u_1 → Sort u_2 → Sort (max u_1 u_2)
#check (Prop → Prop)  -- 输出：Prop → Prop : Sort 1

内容的提问来源于stack exchange，提问作者Chen_zy