Sign.hs revision 3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67
License : GPLv2 or higher, see LICENSE.txt
module HolLight.Sign where
import qualified Data.Map as Map
import Common.DocUtils
import Common.Doc
import Common.Result
import HolLight.Term
import HolLight.Helper
data Sign = Sign { types :: Map.Map String Int
, ops :: Map.Map String HolType }
pretty_types :: Map.Map String Int -> Doc
isSubSig s1 s2 = types s1 `Map.isSubmapOf` types s2
&& ops s1 `Map.isSubmapOf` ops s2