agda - 如何使Agda精美打印产品

考虑下面的独立程序:

 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-1，您将获得:

Goal: .A
————————————————————————————————————————————————————————————
x  : Σ (λ _ → .B)
.B : Set
.A : Set

也就是说，您看到了底层的sigma，而lambda的活页夹类型被隐藏了。这很烦人。有没有一种方法可以使Agda显示默认情况下不绑定名称的活页夹类型？

这是Agda 2.3.2.2。

最佳答案

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需要一种解决这些问题的机制。

关于agda - 如何使Agda精美打印产品，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/30467512/