P.S. I went through Wikipedia's definition a bit more. Not sure it's a full dependent types with the type pairs and stuff. Nim does let you do (constant) value

P.S. I went through Wikipedia's definition a bit more. Not sure it's a full dependent types with the type pairs and stuff. Nim does let you do (constant) value to type conversion with expressions: https://play.nim-lang.org/#ix=4HRz https://play.nim-lang.org/#ix=4HRz or more oddly https://play.nim-lang.org/#ix=4HRA https://play.nim-lang.org/#ix=4HRA . That'd seem to satisfy the `Π` definition and lack of fixed codomain. Though I've never taken a set theory course so YMMV.