%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% BNF of direct-style terms
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

droot : type.  %name droot DROOT.
dexp  : type.  %name dexp DEXP.
dtriv : type.  %name dtriv DTRIV.

dexp->droot : dexp -> droot.

dapp        : dexp -> dexp -> dexp.
dtriv->dexp : dtriv -> dexp.

dlam        : (dtriv -> droot) -> dtriv.