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