% % is-valuetm M: whether a target term M is a value W % is-valuetm : tm -> type. %name is-valuetm _IsValtm. is-valuetm/unit : is-valuetm unittm. is-valuetm/pair : is-valuetm M1 -> is-valuetm M2 -> is-valuetm (pairtm M1 M2). is-valuetm/lam : is-valuetm (lamtm Ebody). is-valuetm/inl : is-valuetm M1 -> is-valuetm (inltm M1). is-valuetm/inr : is-valuetm M2 -> is-valuetm (inrtm M2). %freeze is-valuetm.