Safe Haskell | None |
---|---|
Language | Haskell98 |
Documentation
makeHaskellMeasures :: TCEmb TyCon -> [CoreBind] -> ModName -> (ModName, BareSpec) -> BareM (MSpec SpecType DataCon) Source
makeHaskellInlines :: TCEmb TyCon -> [CoreBind] -> ModName -> (ModName, BareSpec) -> BareM () Source
makeHaskellBounds :: TCEmb TyCon -> CoreProgram -> HashSet (Var, LocSymbol) -> BareM RBEnv Source
makeMeasureSpec' :: MSpec (RType RTyCon RTyVar (UReft Reft)) DataCon -> ([(Var, RType RTyCon RTyVar (UReft Reft))], [(LocSymbol, RRType Reft)]) Source