[Agda] symbol for a singleton set

[Andreas Abel]

On 04.07.2015 22:41, Sergei Meshveliani wrote:
> I observe in  Relation.Unary.agda :
>
>    -- The singleton set.
>    ｛_｝ : A → Pred A a

This seems to be a remainder from when Nisse was fond of using unicode 
versions of reserved ASCII characters.

   FULLWIDTH LEFT CURLY BRACKET

I think he changed his mind, e.g., he does not use

  ∶  (RATION, \:)

for type annotations any more, see module Function in std-lib.

>
> Is this strange symbol intended for the name?
>
> Also type-checking my project sometimes breaks by segmentation fault,
> and it improves after restarting Linux.

Is this due to https://code.google.com/p/agda/issues/detail?id=1518 ?



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

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

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/