liquidhaskell-boot-0.9.10.1.2: Liquid Types for Haskell
Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Bare.Axiom

Description

This module contains the code that DOES reflection; i.e. converts Haskell definitions into refinements.

Documentation

makeHaskellAxioms :: GhcSrc -> Env -> TycEnv -> LogicMap -> GhcSpecSig -> BareSpec -> Lookup [(Var, LocSpecType, Equation)] Source #

strengthenSpecWithMeasure :: GhcSpecSig -> Env -> Var -> LocSymbol -> Located AxiomType Source #

makeAssumeReflectAxioms :: GhcSrc -> Env -> TycEnv -> GhcSpecSig -> BareSpec -> Lookup [(Var, LocSpecType, Equation)] Source #

data AxiomType Source #

Constructors

AT 

Fields

Instances

Instances details
Show AxiomType Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Axiom

Methods

showsPrec :: Int -> AxiomType -> ShowS #

show :: AxiomType -> String #

showList :: [AxiomType] -> ShowS #