> Ya I don't think this is a good definition of dependent type - the prototypical example of a dependent type is a k-length vector. Yah that's why I qualified

> Ya I don't think this is a good definition of dependent type - the prototypical example of a dependent type is a k-length vector. Yah that's why I qualified my statement as dependent type like setup as I don't know a good definition of dependent types which I really grok and I've only briefly dabbled in it. It'd be awesome if you could point out a good resource showing a clear example / simple proof. Well I started working on statically typed vector concepts [1]. The compiler can't do `proc concat[N,M: static int](v1: Vector[N], v2: Vector[M}): Vector[N+M]` and it fails. It might be able to be implemented via a macro like `proc concat(v1: Vector[N], v2: Vector[M}): typeFromSumOf(N,M)`, but I haven't tried yet. Also just using static ints would require specific values at some point to work I think. Whereas you'd really want "induction" of some sort. Maybe a SAT solver would be required at that point? There's DrNim [2] which does tie Z3 but it's sorta dormant. > Um yes this is literally what I was asking with respect to top ⊤. Ah, I didn't know what you meant by top T. > ya the negation is interesting - I wonder how it's implemented. Nim's VM runs from Nim AST, so probably running it as a VM expression. 1: https://github.com/elcritch/platonic https://github.com/elcritch/platonic 2: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html