Language.Why3.CSE

Documentation

cseFormula :: (Int, Expr) -> (Int, Expr)

The Int is the seed to generate names. If cseFormula is called multiple times, one should take care to supply a new name seed, to avoid clashing names.

type Shape = Expr

type Simple = Expr

data S

Constructors

S

Fields

sMap :: !(Map Shape (Int, Simple))

sNext :: !Int

Instances

Show S

type M = StateT S Lift

importFormula :: Expr -> M Expr

importTerm :: Expr -> M Simple

compound :: ([Simple] -> Shape) -> [Expr] -> M Simple

varName :: Int -> Text