[tel]

It's a bit more than that. Let's assume Vector is a typed list type of know length

    [1,2,3] : Vector 3 Int

we can write `append` which combines Vectors

    append : (Vector n a, Vector m a) -> Vector (n + m) a

which works as you expect because the expression in the type (n+m) is written in the value language.

Here's another (slightly pathological) dependent type. Normally `if` statements require that the then and the else branches result in the same type, but in a DT language you can write

    if' : (cond : Bool) -> a -> b -> (if cond then a else b)

In other words, `if'` takes the type where you first provide it a boolean, we'll call it `cond`, and then two differently type continuation parameters. The type of the result is an expression: "if cond is true then this is the type of the first continuation, otherwise this is the type of the second continuation".

Both of these examples would be proud to call themselves trivial. The DT rabbit hole goes very deep.