| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Types.Graduals
Description
This module contains the top-level SOLUTION data types, including various indices used for solving.
Documentation
uniquify :: (NFData a, Fixpoint a, Loc a) => SInfo a -> SInfo a Source #
Make each gradual appearence unique -------------------------------------
makeSolutions :: (NFData a, Fixpoint a, Show a) => Config -> SInfo a -> [(KVar, (GWInfo, [[Expr]]))] -> Maybe [GSol] Source #
class Gradual a where Source #
Substitute Gradual Solution ---------------------------------------------
Instances
| Gradual SortedReft Source # | |
Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> SortedReft -> SortedReft Source # | |
| Gradual Reft Source # | |
| Gradual Expr Source # | |
| Gradual BindEnv Source # | |
| Gradual (SInfo a) Source # | |
| Gradual (SimpC a) Source # | |
| Gradual v => Gradual (HashMap k v) Source # | |
Defined in Language.Fixpoint.Types.Graduals | |