Conversation

Notices

1. Embed this notice
   julesh (julesh@mathstodon.xyz)'s status on Wednesday, 27-Nov-2024 02:21:20 JST julesh

   • Zanzi @ Monoidal Cafe
   • G. Allais
   • alahijani
   • Jan de Muijnck-Hughes

   @zanzi @gallais @alahijani @jfdm @edwinb Oh yeah, I've considered that most things on reddit have been lost since a few years ago

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

     in reply to

     • G. Allais
     • alahijani
     • Jan de Muijnck-Hughes

     @julesh @gallais @alahijani @jfdm @edwinb If it helps, the post just links to this gist by @gallais https://github.com/gallais/potpourri/blob/main/agda/poc/LinearDec.agda
     What is the equivalent of "inspect" in idris? Is it just `with`?