8.2 带依赖类型的演算 ·上下文T T:=☑|T,x:oT,t:k 项变量的类型约束、类型变量的种类约束 把Γ看成有序的，设计证明系统来证明上下文良 形与否并不困难 下面把T看成无序的集合，以简化定类规则和定 型规则的设计8.2 带依赖类型的演算 • 上下文  ::=  | , x : | , t : k – 项变量的类型约束、类型变量的种类约束 – 把看成有序的，设计证明系统来证明上下文良 形与否并不困难 – 下面把看成无序的集合，以简化定类规则和定 型规则的设计