:: Term s (PValue _ a :--> PValue _ a) is:exact package:plutarch

Value without any non-Ada
Value without any Ada
Assert all amounts in the value are positive.