-- ========================================================================
--        declarations of constants and literals for ABP
-- ========================================================================

-- ========================================================================
require abp-sys

-- ========================================================================
-- arbitrary constants and constant literals
mod* CONST-LITL {ex(CONFIG)
-- arbitray constants; fresh constants
ops src1 src2 : -> SrCh . 
ops ns1 ns2 : -> NnSeq .
ops rsc1 rsc2 : -> RsCh . 
-- Nn literals 
[NnLt < Nn]
ops n1 n2 n3 : -> NnLt .
-- an equation for literals of sort NnLt
eq (N1:NnLt = N2:NnLt) = (N1 == N2) .
-- Bnp literals
[BnpLt < Bnp]
ops bn1 bn2 bn3 : -> BnpLt .
eq (BN1:BnpLt = BN2:BnpLt) = (BN1 == BN2) .
}

-- ========================================================================
provide abp-constLitl

-- ========================================================================
eof