Consider the following self-contained program:
module Test where
record Σ {A : Set} (B : A -> Set) : Set where
constructor _,_
field
fst : A
snd : B fst
open Σ public
infixr 0 _,_
_×_ : Set -> Set -> Set
A × B = Σ (\ (_ : A) -> B)
infixr 10 _×_
f : {A B : Set} → A × B → A
f x = {!!}
如果你在目标中使用 C-c C-l,你会得到:
Goal: .A
————————————————————————————————————————————————————————————
x : Σ (λ _ → .B)
.B : Set
.A : Set
也就是说,你看到了底层的 sigma(类型),但是 lambda 绑定器的类型被隐藏了。这非常令人困扰。有没有办法让 Agda 默认显示不绑定名称的绑定器的类型?
这是 Agda 2.3.2.2 版本。