liquid-fixpoint-0.6.0.1: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Language.Fixpoint.Solver.Instantiate
Contents
Description
Axiom Instantiation ------------------------------------------------------
instantiateAxioms :: Config -> Context -> BindEnv -> SEnv Sort -> AxiomEnv -> Integer -> SubC c -> IO (SubC c) Source #
instantiateFInfo :: Config -> Context -> FInfo c -> IO (FInfo c) Source #
Methods
expr :: (Symbol, SortedReft) -> Expr Source #