- measures :: ![Measure ty bndr]
User-defined properties for ADTs
- asmSigs :: ![(LocSymbol, ty)]
Assumed (unchecked) types
- sigs :: ![(LocSymbol, ty)]
Imported functions and types
- localSigs :: ![(LocSymbol, ty)]
Local type signatures
- invariants :: ![Located ty]
Data type invariants
- ialiases :: ![(Located ty, Located ty)]
Data type invariants to be checked
- imports :: ![Symbol]
Loaded spec module names
- dataDecls :: ![DataDecl]
Predicated data definitions
- includes :: ![FilePath]
Included qualifier files
- aliases :: ![RTAlias Symbol BareType]
RefType aliases
- paliases :: ![RTAlias Symbol Pred]
Refinement/Predicate aliases
- ealiases :: ![RTAlias Symbol Expr]
Expression aliases
- embeds :: !(TCEmb LocSymbol)
GHC-Tycon-to-fixpoint Tycon map
- qualifiers :: ![Qualifier]
Qualifiers in source/spec files
- decr :: ![(LocSymbol, [Int])]
Information on decreasing arguments
- lvars :: ![LocSymbol]
Variables that should be checked in the environment they are used
- lazy :: !(HashSet LocSymbol)
Ignore Termination Check in these Functions
- hmeas :: !(HashSet LocSymbol)
Binders to turn into measures using haskell definitions
- inlines :: !(HashSet LocSymbol)
Binders to turn into logic inline using haskell definitions
- pragmas :: ![Located String]
Command-line configurations passed in through source
- cmeasures :: ![Measure ty ()]
Measures attached to a type-class
- imeasures :: ![Measure ty bndr]
Mappings from (measure,type) -> measure
- classes :: ![RClass ty]
Refined Type-Classes
- termexprs :: ![(LocSymbol, [Expr])]
Terminating Conditions for functions
- rinstance :: ![RInstance ty]
-
- dvariance :: ![(LocSymbol, [Variance])]
-