Clever Geek Handbook

How to make beautiful Agda products beautiful

Consider the following stand-alone 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 = {!!}

If you Cc Cl targets, you get:

Goal: .A
β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”
x  : Ξ£ (Ξ» _ β†’ .B)
.B : Set
.A : Set

i.e. you see basic sigma and the lambda binder type is hidden. This is pretty annoying. Is there a way to get Agda to show the type of binders that do not bind names by default?

This is Agda 2.3.2.2.

+3


source to share


2 answers


Agda 2.4.3 displays x : .A Γ— .B

.

You can use the abstract keyword :

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


But this is definitely overkill (and it looks like pattern synonyms don't work in abstract blocks).

I find it much more annoying that Agda doesn't want to downsize type functions flip

and especially _∘_

, but deploys some functions with really long definitions. Agda needs a mechanism to fix these problems.

+2


source


It looks like this issue has been fixed in the latest version of Agda, so you should update it.



+1


source






More articles:


All Articles