jules-hedges

jules-hedges / Cases.idr

Last active December 18, 2024 11:16

A simple implementation of non-nested patterns, desugaring to eliminators

	data Simplex : List a -> List a -> List a -> Type where
	Z : Simplex [] ys ys
	S : Simplex xs ys zs -> Simplex (x :: xs) ys (x :: zs)

	data Ty : Type where
	Unit : Ty
	Prod : Ty -> Ty -> Ty
	Sum : Ty -> Ty -> Ty
	Hom : Ty -> Ty -> Ty