Public
- Public
- Network
- Groups
- Featured
- Popular
- People

Conversation

Notices

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 conversation about 2 months ago from mathstodon.xyz permalink
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
- Embed this notice
  Jade Master (jademastermath@mathstodon.xyz)'s status on Saturday, 14-Dec-2024 22:21:11 JST Jade Master
  in reply to
  
  @julesh I'm glad that we're using jists now btw, I think they're nice
  
  In conversation about 2 months ago permalink

Public

Conversation

Notices

Feeds