search

DIJamner / InDependent

A gradual, dependently typed language
7 stars 1 forks source link

ADTs should have variable types #1

Closed DIJamner closed 9 years ago

DIJamner commented 9 years ago

Structures like the following should be implemented:

data Vec : Type1 -> Int -> Type1 { empty : (Vec 0) cons : {t:Type1} -> t -> (Vec t i) -> (Vec t (add i 1))

}

Note: requires some amount of pattern matching on ADTs.

DIJamner commented 9 years ago

This has been implemented.