Recent searches
Search options
I came up with a much simpler way to do (non-nested) patterns
Full code: https://gist.github.com/jules-hedges/69a07606c1f0100682daeb5d82885296
![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 "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)")
@julesh I'm glad that we're using jists now btw, I think they're nice
I came up with a much simpler way to do (non-nested) patterns
Full code: https://gist.github.com/jules-hedges/69a07606c1f0100682daeb5d82885296
@julesh I'm glad that we're using jists now btw, I think they're nice