什么是精益中有效的类型？
什么是精益中有效的类型？
提问于 2016-12-07 20:42:34
我已经完成了精益教程的前三章，并且已经完成了命题逻辑中的几个证明。
现在我正试着回到过去，问自己愚蠢的问题。
我的理解是：
- 术语可以有类型：
constant A : Type。A是一个术语，Type是A的类型。 - 术语可以变成类型：
constant a : A。 - 术语的类型可以依赖于另一个术语的类型：
constant B : A -> Type，它是constant B' : Π (a : A), Type的糖
但是这种理解显然是错误的，因为这段代码并不是打字机：
constant A : Type
constant a : A
constant B : A -> Type
constant B' : Π (a : A), Type
constant C : Π (b : B), Type
constant C' : Π (B : A), (Π (b : B), Type)
constant C'' : B -> Type所有以constant C开头的行，即第9、11和13行都抛出一个错误error: type expected at B
为什么？我怀疑不是所有的术语都可以成为类型。我怀疑类型依赖于其他类型的术语不会变成类型。为什么？
回答 1
Stack Overflow用户
回答已采纳
发布于 2016-12-08 10:09:01
第一类误差
中的第一个类型错误的问题
constant C : Π (b : B), Type您不能说b : B，因为B是A -> Type类型的函数(没有定义)，也就是说B是一个值，而不是一个类型。提出像b : 1、b : "xyz"或b : (λ a : A, Type)这样的声明是没有意义的。
例如，由于B a : Type，以下内容将起作用：
constant C : Π (b : B a), Type第二类误差
第二种类型的错误
constant C' : Π (B : A), (Π (b : B), Type)由于不知道B是一种类型，我们对B所知道的就是它是A类型的一些值(居民)。为了能够以这种方式使用B，您需要如下所示：
constant C' : Π (B : Type), (Π (b : B), Type)也就是说，我们明确地说B是一种类型。
第三类误差
constant C'' : B -> Type这对打字机失败的原因和第一种情况是一样的。B是一个函数值，而我们在这里需要一个类型--这就是constant B : A -> Type工作的原因。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/41026997
复制相关文章
相似问题
腾讯云开发者
