小编kks*_*kai的帖子

例如，这不是尾调用：

map _ [] = []
map f (x : xs) = f x : map f xs

由(:)数据构造函数保护的递归调用，因此它不会像其他语言中的等价物那样构建巨大的堆栈。它是这样工作的：

map (+1) (1 : 2 : 3 : [])
2 : map (+1) (2 : 3 : [])
2 : 3 : map (+1) (3 : [])
2 : 3 : 4 : map (+1) []
2 : 3 : 4 : []

为什么不

map (+1) (1 : 2 : 3 : [])
2 : map (+1) (2 : …

我在plfa读到这样一段代码。

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_?_; refl; cong; sym)
open Eq.?-Reasoning using (begin_; _???_; _??_?_; _?)

但_??_?_不在命题平等中

The module Eq.?-Reasoning doesn't export the following: _??_?_
when scope checking the declaration
  open Eq.?-Reasoning using (begin_; _???_; _??_?_; _?)

我只在Function.Related和 中找到它Relation.Binary.HeterogeneousEquality。怎么了？