Embed Notice

HTML Code

<blockquote style="position: relative; padding-left: 55px;"><section><a href="https://mathstodon.xyz/users/zanzi/statuses/113550528464968300">Zanzi @ Monoidal Cafe (zanzi@mathstodon.xyz)'s status on Wednesday, 27-Nov-2024 02:52:45 JST</a><a href="https://mathstodon.xyz/@zanzi" title="zanzi@mathstodon.xyz"><img src="https://gnusocial.jp/avatar/238194-48-20240126140557.webp" width="48" height="48" alt="Zanzi @ Monoidal Cafe" style="position: absolute; left: 0; top: 0;">Zanzi @ Monoidal Cafe</a><div><a href="https://mathstodon.xyz/@julesh/113550400869192582" rel="in-reply-to">in reply to</a><ul><li><li><a href="https://gnusocial.jp/user/300502" title="gallais@piaille.fr">G. Allais</a></li><li><a href="https://gnusocial.jp/user/300503" title="alahijani@mathstodon.xyz">alahijani</a></li><li><a href="https://gnusocial.jp/user/300505" title="jfdm@discuss.systems">Jan de Muijnck-Hughes</a></li></ul></div></section><article><p><a href="https://mathstodon.xyz/@julesh">@julesh</a> <a href="https://piaille.fr/@gallais">@gallais</a> <a href="https://mathstodon.xyz/@alahijani">@alahijani</a> <a href="https://discuss.systems/@jfdm">@jfdm</a> <a href="https://types.pl/@edwinb">@edwinb</a> If it helps, the post just links to this gist by @gallais <a href="https://github.com/gallais/potpourri/blob/main/agda/poc/LinearDec.agda" rel="nofollow noreferrer">https://github.com/gallais/potpourri/blob/main/agda/poc/LinearDec.agda</a> <br>What is the equivalent of "inspect" in idris? Is it just `with`?</p></article><footer><a rel="bookmark" href="https://gnusocial.jp/conversation/4075224#notice-7963338">In conversation</a><time datetime="2024-11-27T02:52:45+09:00" title="Wednesday, 27-Nov-2024 02:52:45 JST">about 6 months ago</time> <span>from <span><a href="https://gnusocial.jp/notice/7963338" rel="external" title="Sent from gnusocial.jp via ActivityPub">gnusocial.jp</a></span></span><a href="https://gnusocial.jp/notice/7963338">permalink</a><h4>Attachments</h4><ol><li><article><header><div>Domain not in remote thumbnail source whitelist: opengraph.githubassets.com</div><h5><a href="https://github.com/gallais/potpourri/blob/main/agda/poc/LinearDec.agda">potpourri/agda/poc/LinearDec.agda at main · gallais/potpourri</a></h5><div></div></header><div>Where my everyday research happens. Contribute to gallais/potpourri development by creating an account on GitHub.</div><footer></footer></article></li></ol></footer></blockquote>

Corresponding Notice

Embed this notice
Zanzi @ Monoidal Cafe (zanzi@mathstodon.xyz)'s status on Wednesday, 27-Nov-2024 02:52:45 JSTZanzi @ Monoidal Cafe
in reply to
@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`?
In conversationabout 6 months ago from gnusocial.jppermalink
Attachments
1. Domain not in remote thumbnail source whitelist: opengraph.githubassets.com
  potpourri/agda/poc/LinearDec.agda at main · gallais/potpourri
  Where my everyday research happens. Contribute to gallais/potpourri development by creating an account on GitHub.

Public

Embed Notice

HTML Code

Corresponding Notice