% A term N of type nat is a nonnegative integer. % Constructors: 0, 1. nat: type. %name nat N. 0: nat. 1: nat -> nat. %prefix 200 1. % The judgment (N1 ==nat N2) means that N1 is equal to N2. ==nat: nat -> nat -> type. %name ==nat E. %infix none 100 ==nat. ==nat_refl: N ==nat N. % addition +nat : nat -> nat -> nat -> type. %mode +nat +N1 +N2 -N3. - : +nat 0 N N. - : +nat (1 N1) N2 (1 N3) <- +nat N1 N2 N3. %worlds () (+nat _ _ _). %total {N1} (+nat N1 _ _).