-include "arithmetics/nat.ma".
-
-inductive T : Type[0] ≝
- | Sort: nat → T (* starts from 0 *)
- | Rel: nat → T (* starts from ... ? *)
- | App: T → T → T (* function, argument *)
- | Lambda: T → T → T (* type, body *)
- | Prod: T → T → T (* type, body *)
- | D: T → T (* dummifier *)
-.