Conversation

My first Agda code, for an exercise of the Type Theory course at MGS. Looks very cute 🥰 I must confess I never used Agda before mostly because I was intimidated by having to use emacs. But it turns out emacs is a lot easier to use than vim (for a beginner).

Screenshot of a snippet of code written in Agda. Syntax highlighting colors the code in orange, pink, purple, white and green. The code uses several Unicode mathematical symbols, like an actual lambda for a lambda abstraction.

read image description

ALT

4

3

If you’d like to talk about related things, you could join us in ##dependent on libera.chat IRC.

A next-generation IRC network for FOSS projects collaboration!

1

1

Brendan Zabarauskas

Replying to

and

Oh, just found that matrix has been bridged to libera! So yeah, joined again (I used to lurk on the freenode one).

2:50 AM · Jun 18, 2021Twitter Web App