agda - 废话 "Not in scope"错误

Question

有时 Agda 会给我一些无意义的“不在范围内”错误，让我不知道该怎么做。下面是一个例子:

open import Data.Product
open import Data.Bool
open import Data.Unit

postulate
  μ    : (Set → Set) → Set
  In   : {F : Set → Set} → F (μ F) → μ F
  unIn : {F : Set → Set} → μ F → F (μ F)

NatT : Set
NatT = μ λ x -> Σ Bool (λ { true -> ⊤; false -> x })

x : NatT
x = In (false , In (true, tt))

这个投诉 true不在范围内。考虑到 x = In (true, tt)，这就更奇怪了工作正常。为什么会发生这种情况？

Not in scope:
  true, at /Users/v/agda/mu.agda:14,21-26
    (did you mean
       'Bool.true' or
       'Data.Bool.Bool.true' or
       'Data.Bool.true' or
       'true'?)
when scope checking true,

Answer 1

缺少空格。正确:

x = In (false , In (true , tt))

Agda 说 true,不在范围内；请注意 , . Agda 将大多数无空格字符序列视为单个标记，这很奇怪，但通常很有用。