19. 基本命题
除了蕴含和全称量词外，逻辑连接词和量词都在 Prop 宇宙中实现为 归纳类型。
从某种意义上说，本章介绍的连接词并不特殊——任何用户都可以实现它们。
不过，标准库和内置证明自动化工具广泛使用了这些基本连接词。
除了蕴含和全称量词外，逻辑连接词和量词都在 Prop 宇宙中实现为 归纳类型。
从某种意义上说，本章介绍的连接词并不特殊——任何用户都可以实现它们。
不过，标准库和内置证明自动化工具广泛使用了这些基本连接词。