Conversation

Notices

1. Embed this notice
   Jan de Muijnck-Hughes (jfdm@discuss.systems)'s status on Wednesday, 27-Nov-2024 02:21:10 JST Jan de Muijnck-Hughes

   in reply to

   • julesh
   • Zanzi @ Monoidal Cafe

   @zanzi @edwinb @julesh

   There _are_ tricks one can use to make writing DecEq proofs easier (diagonals; decDo-notation). It is all about the cases...

   There maybe deriving for simple types using elab reflection. I am, however, am not an advanced Idris programmer [1] so YMMV.

   We can also do better than `Dec`, but what do I know...

   [1] no matter what others in this thread would say...

   • Embed this notice
     Zanzi @ Monoidal Cafe (zanzi@mathstodon.xyz)'s status on Wednesday, 27-Nov-2024 02:21:11 JST Zanzi @ Monoidal Cafe

     • julesh

     @edwinb @julesh oh yes, I have been writing a bunch of manual instances recently so I can relate. Automating equation generation would be a killer feature imo!