相关疑难解决方法(0)

我目前正在使用Idris书籍进行类型驱动开发.

我在第6章中有两个与示例数据存储设计有关的问题.数据存储是一个命令行应用程序,允许用户设置存储在其中的数据类型,然后添加新数据.

以下是代码的相关部分(略有简化).你可以在Github上看到完整的代码:

module Main

import Data.Vect

infixr 4 .+.

-- This datatype is to define what sorts of data can be contained in the data store.
data Schema
  = SString
  | SInt
  | (.+.) Schema Schema

-- This is a type-level function that translates a Schema to an actual type.
SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

-- …

我来自JavaScript/Ruby编程背景,我习惯这是真/假的工作原理(在JS中):

!true
// false
!false
// true

然后你就可以使用这些真/假值与&&像

var a = true, b = false;
a && !b;

所以,而不是(和其他逻辑/布尔运算符)是单个系统的一部分; 似乎"逻辑"系统和"布尔"系统是同一个系统.

但是,在Coq中,逻辑和布尔值是两个不同的东西.为什么是这样？下面的引用/链接演示了如何将定理与它们联系起来.

我们已经看到过几个可以在Coq的计算(类型)和逻辑(Prop)世界中找到类似结构的地方.还有一个:布尔运算符andb和orb显然是逻辑连接词的类似物？和？通过以下定理可以使这种类比更加精确,这些定理表明如何将关于orb和orb在某些输入上的行为的知识转化为关于这些输入的命题事实.

Theorem andb_prop : ?b c,
  andb b c = true ? b = true ? c = true.

Run Code Online (Sandbox Code Playgroud)

http://www.seas.upenn.edu/~cis500/current/sf/Logic.html#lab211

我想知道,coq中是否有一个常用的矢量库,即它们的类型长度索引.

有些教程引用了Bvector,但是当我尝试导入它时却找不到它.

有Coq.Vectors.Vectordef,但是那里定义的类型只是命名t,这使我认为它是供内部使用的.

对于不想推出自己的图书馆的人来说,最好或最常见的做法是什么？我对标准库中的向量有误吗？还是有另一个我失踪的自由人？或者人们只是使用列表,并与他们的长度证明配对？