• Public

  • Public
  • Network
  • Groups
  • Featured
  • Popular
  • People

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)