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.

Synopsis

Documentation

Make each gradual appearence unique -------------------------------------

Instances

Show GSol Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods showsPrec :: Int -> GSol -> ShowS # show :: GSol -> String # showList :: [GSol] -> ShowS #
Semigroup GSol Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods (<>) :: GSol -> GSol -> GSol # sconcat :: NonEmpty GSol -> GSol # stimes :: Integral b => b -> GSol -> GSol #
Monoid GSol Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods mempty :: GSol # mappend :: GSol -> GSol -> GSol # mconcat :: [GSol] -> GSol #

class Gradual a where Source #

Substitute Gradual Solution ---------------------------------------------

Methods

Instances

Gradual SortedReft Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> SortedReft -> SortedReft Source #
Gradual Reft Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> Reft -> Reft Source #
Gradual Expr Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> Expr -> Expr Source #
Gradual BindEnv Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> BindEnv -> BindEnv Source #
Gradual (SInfo a) Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> SInfo a -> SInfo a Source #
Gradual (SimpC a) Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> SimpC a -> SimpC a Source #
Gradual v => Gradual (HashMap k v) Source #
Instance details Defined in Language.Fixpoint.Types.Graduals Methods gsubst :: GSol -> HashMap k v -> HashMap k v Source #