370
个编辑
更改
跳到导航
跳到搜索
第198行：
第198行： − + − 头部<code>head</code>是字符串，且+ − 尾部<code>tail</code>是字符串流。+
→协归纳定义的数据和共递归
tail(s) is a stream of strings.
tail(s) is a stream of strings.
字符串流是s这样的对象：
字符串流是s这样的对象：
头部<code>head</code>是字符串，且
尾部<code>tail</code>是字符串流。
This is very similar to an inductive definition of lists of strings; the difference is that this definition specifies how to access the contents of the data structure—namely, via the [[accessor]] functions <code>head</code> and <code>tail</code>—and what those contents may be, whereas the inductive definition specifies how to create the structure and what it may be created from.
This is very similar to an inductive definition of lists of strings; the difference is that this definition specifies how to access the contents of the data structure—namely, via the [[accessor]] functions <code>head</code> and <code>tail</code>—and what those contents may be, whereas the inductive definition specifies how to create the structure and what it may be created from.