如何使Agda漂亮地打印产品

Question

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 版本。

- Edward Z. Yang

Answer 1

Agda 2.4.3 显示 x : .A × .B。

你可以使用 abstract 关键字：

abstract
  _×_ : Set -> Set -> Set
  A × B = Σ (\ (_ : A) -> B)

  fst' : ∀ {A B} -> A × B -> A
  fst' (x , y) = x

  snd' : ∀ {A B} -> A × B -> B
  snd' (x , y) = y

但这肯定是过度的（并且似乎模式同义词在抽象块中不起作用）。

对我来说更加烦人的是，Agda不想减少像flip和尤其是_∘_这样的函数，而是展开一些定义非常长的函数。 Agda需要一个机制来解决这些问题。

- effectfully

Answer 2

看起来这个问题已经在最新版本的Agda中得到了修复，因此您应该升级。

- Edward Z. Yang