Conversation

Notices

1. Embed this notice
   quat (steady and true) (quat@woof.group)'s status on Saturday, 28-Dec-2024 13:25:46 JST quat (steady and true)

   in reply to

   "Are you using lean as a general purpose functional language and not really touching the theorem prover" Yeah why not, it's fun!!

   • kuteboiCoder likes this.
   • Embed this notice
     quat (steady and true) (quat@woof.group)'s status on Saturday, 28-Dec-2024 13:25:47 JST quat (steady and true)

     Lean has like super-hyper-turbo uniform function call syntax where the "receiver" doesn't have to actually be the first argument to the function, which is extremely sickos.png and a lot of fun, but also very confusing when you're learning since `x.map y` might desugar to either `map x y` or `map y x` depending how the types line up

     kuteboiCoder repeated this.