术语表（完善中）
繁饰 elaboration
抽象 abstraction
应用 application
合一 unification
规约 Reduction
策略 tactic
组合子 combinator
构造子 constructor
消去子 eliminator
递归子 recursor
构造演算 Calculus of Constructions
归纳类型 inductive type
依值类型论 dependent type theory