[Agda] nullary copattern matching

[Andreas Abel]

 > What is the syntax for copattern matching on a record with zero fields?

There isn't any yet, although Jesper and I discussed adding it:

   record True : Set where

   triv : True
   triv .()

The syntax would be a post-fix absurd projection pattern.

Do you have an interesting application for it?  With eta-equality, there 
is not so much use it seems, since the same can be obtained by

   triv = _

Cheers,
Andreas

On 20.03.2018 23:12, Christian Sattler wrote:
> What is the syntax for copattern matching on a record with zero fields? 
> I could not find anything in the documentation. For pattern matching on 
> a data type with zero constructors, we have syntax for denoting an 
> impossible case, but what about the analogous situation for copatterns? 
> Note that C-c C-c will happily produce invalid code ("missing definition").
> 
> Christian
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/