<div dir="ltr"><div>> Anyway, the main thing here is to formulate clearly for oneself:<br>> what is the goal of the project.<br></div><div><br></div>I want to experience function-level programming (point-free style) via Agda. So I chose direct way of defining combinators in Agda instead of to define the grammar and semantics of combinatory logic.</div>