[Agda] symbol for a singleton set

Sergei Meshveliani mechvel at botik.ru
Sat Jul 4 22:41:16 CEST 2015


People,

I observe in  Relation.Unary.agda :

  -- The singleton set.   
  {_} : A → Pred A a   

Is this strange symbol intended for the name? 

Also type-checking my project sometimes breaks by segmentation fault,
and it improves after restarting Linux. 

(I suspect that something is corrupted in the emacs mode or in files, or
in the hardware). 

Thanks,

------
Sergei

 



More information about the Agda mailing list