[Agda] Problem with \lambda

Andreas Abel abela at chalmers.se
Tue Mar 8 10:27:42 CET 2016


> On 2016-03-04 16:57,   wrote:
>> Agda doesn't permit \lambda as a type constructor!

You can use the character

   http://www.fileformat.info/info/unicode/char/019b/index.htm

instead of lambda.  Anyway, you cannot use juxtaposition for application 
either, as it is Agda's application.

-- 
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/


More information about the Agda mailing list