依赖类型

一种高级类型系统机制，允许类型本身依赖于运行时值，使得数组不越界、函数输入约束等性质可在编译期静态保证，是Lean、Coq、Idris等形式化验证语言的核心基础