Embed Notice

HTML Code

<blockquote style="position: relative; padding-left: 55px;"><section><a href="https://mathstodon.xyz/users/julesh/statuses/113651322630501759">julesh (julesh@mathstodon.xyz)'s status on Saturday, 14-Dec-2024 22:06:01 JST</a><a href="https://mathstodon.xyz/@julesh" title="julesh@mathstodon.xyz"><img src="https://gnusocial.jp/avatar/180791-48-20231002164329.webp" width="48" height="48" alt="julesh" style="position: absolute; left: 0; top: 0;">julesh</a></section><article><p>I came up with a much simpler way to do (non-nested) patterns</p><p>Full code: <a href="https://gist.github.com/jules-hedges/69a07606c1f0100682daeb5d82885296" rel="nofollow noreferrer">https://gist.github.com/jules-hedges/69a07606c1f0100682daeb5d82885296</a></p></article><footer><a rel="bookmark" href="https://gnusocial.jp/conversation/4184959#notice-8178820">In conversation</a><time datetime="2024-12-14T22:06:01+09:00" title="Saturday, 14-Dec-2024 22:06:01 JST">about 2 months ago</time> <span>from <span><a href="https://mathstodon.xyz/@julesh/113651322630501759" rel="external" title="Sent from mathstodon.xyz via ActivityPub">mathstodon.xyz</a></span></span><a href="https://mathstodon.xyz/@julesh/113651322630501759">permalink</a><h4>Attachments</h4><ol><li><label><a rel="external" href="https://gnusocial.jp/attachment/3697473">mutual
  namespace Cases
    public export
    -- `Cases a xs b` is something that case splits on a variable of type `a`,
    -- branches share free variables in `xs`, and the whole thing has type `b`
    data Cases : Ty -&gt; List Ty -&gt; Ty -&gt; Type where
      Var : Term (a :: xs) b -&gt; Cases a xs b
      Unit : Term xs a -&gt; Cases Unit xs a
      Pair : Term (a :: b :: xs) c -&gt; Cases (Prod a b) xs c
      Sum : Term (a :: xs) c -&gt; Term (b :: xs) c -&gt; Cases (Sum a b) xs c  namespace Original
    public export
    data Term : List Ty -&gt; Ty -&gt; Type where
      Var : Term [x] x
      Let : Simplex xs ys zs -&gt; Term xs a -&gt; Cases a ys b -&gt; Term zs b
      Pair : Simplex xs ys zs -&gt; Term xs a -&gt; Term ys b -&gt; Term zs (Prod a b)
      Left : Term xs a -&gt; Term xs (Sum a b)
      Right : Term xs b -&gt; Term xs (Sum a b)</a></label><br><a href="https://media.mathstodon.xyz/media_attachments/files/113/651/317/782/032/552/original/bc19bdb432343741.png" rel="external">https://media.mathstodon.xyz/media_attachments/files/113/651/317/782/032/552/original/bc19bdb432343741.png</a></li><li><article><header><div>Domain not in remote thumbnail source whitelist: github.githubassets.com</div><h5><a href="https://gist.github.com/jules-hedges/69a07606c1f0100682daeb5d82885296">A simple implementation of non-nested patterns, desugaring to eliminators</a></h5><div> from <span>jules-hedges</span></div></header><div>A simple implementation of non-nested patterns, desugaring to eliminators</div><footer></footer></article></li></ol></footer></blockquote>

Corresponding Notice

Embed this notice
julesh (julesh@mathstodon.xyz)'s status on Saturday, 14-Dec-2024 22:06:01 JST julesh
I came up with a much simpler way to do (non-nested) patterns
Full code: https://gist.github.com/jules-hedges/69a07606c1f0100682daeb5d82885296
In conversationabout 2 months ago from mathstodon.xyzpermalink
Attachments
1. mutual namespace Cases public export -- `Cases a xs b` is something that case splits on a variable of type `a`, -- branches share free variables in `xs`, and the whole thing has type `b` data Cases : Ty -> List Ty -> Ty -> Type where Var : Term (a :: xs) b -> Cases a xs b Unit : Term xs a -> Cases Unit xs a Pair : Term (a :: b :: xs) c -> Cases (Prod a b) xs c Sum : Term (a :: xs) c -> Term (b :: xs) c -> Cases (Sum a b) xs c namespace Original public export data Term : List Ty -> Ty -> Type where Var : Term [x] x Let : Simplex xs ys zs -> Term xs a -> Cases a ys b -> Term zs b Pair : Simplex xs ys zs -> Term xs a -> Term ys b -> Term zs (Prod a b) Left : Term xs a -> Term xs (Sum a b) Right : Term xs b -> Term xs (Sum a b)
  https://media.mathstodon.xyz/media_attachments/files/113/651/317/782/032/552/original/bc19bdb432343741.png
2. Domain not in remote thumbnail source whitelist: github.githubassets.com
  A simple implementation of non-nested patterns, desugaring to eliminators
  from jules-hedges
  A simple implementation of non-nested patterns, desugaring to eliminators

Public

Embed Notice

HTML Code

Corresponding Notice