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

-- ========================================================================
require qlock-sys

-- ========================================================================
-- arbitrary constants and constant literals
mod* CONSTandLITL {ex(STATE)
-- arbitray constants; fresh constants
op q : -> Qu . 
op as : -> Aobs .
-- Aid literals 
[AidLt < Aid]
ops a1 a2 a3 : -> Aid .
-- an equation for literals of sort AidLt
eq (B1:AidLt = B2:AidLt) = (B1 == B2) .
-- arbitrary Aid constant literals
ops b1 b2 b3 : -> AidLt .
}

-- ========================================================================
provide qlock-constAndLitl

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