[Agda] \member vs \notin

Serge D. Mechveliani mechvel at botik.ru
Mon Feb 4 12:43:26 CET 2013

When I look at  foo.agda  with  emacs  under the Agda mode,
and request on the "\notin" symbol (by positionning at it in the text),
emacs  prints
   to input: type "\notin" or "\inn" or "\member" with Agda

But "\member" is a membership symbol, is is already occupied,
while  "\notin"  is for non-membership.  
I do not know,
is this a typo in the  agda-mode  doc part for emacs ?,
in UTF-8 doc in emacs ?



More information about the Agda mailing list