← Back to context

Comment by p1esk

5 hours ago

I didn’t understand that notation. Can someone please explain?

I think:

   x => a

is:

   λx. a 

and

   f <- a

is just application. I.e.

   f a

  • What about big T, square/angle brackets, and braces?

    • T is a translation function, square brackets indicate a term within another term (its context), and braces are standard substitution. It's deliberately vague to make discovery more fun (I know this is very controversial, but the most fun papers/articles I read are the ones whose notation I don't understand at all)

      I try to give just about enough information to be able to understand it given some time and experimentation.