Safe Haskell | None |
---|---|
Language | Haskell98 |
Documentation
makeHaskellMeasures :: TCEmb TyCon -> [CoreBind] -> BareSpec -> BareM [Measure (Located BareType) LocSymbol] Source #
makeMeasureSpec' :: MSpec SpecType DataCon -> ([(Var, SpecType)], [(LocSymbol, RRType Reft)]) Source #
makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t -> [(LocSymbol, CMeasure (RType c tv r2))] Source #
makeMeasureSelectors :: Bool -> Bool -> (DataCon, Located DataConP) -> [Measure SpecType DataCon] Source #
strengthenHaskellMeasures :: HashSet (Located Var) -> [(Var, LocSpecType)] -> [(Var, LocSpecType)] Source #
strengthenHaskellInlines :: HashSet (Located Var) -> [(Var, LocSpecType)] -> [(Var, LocSpecType)] Source #