@hackage liquid-fixpoint0.9.2.5

This package implements an SMTLIB based Horn-Clause/Logical Implication constraint solver used for Liquid Types.

The package includes:

1. Types for Expressions, Predicates, Constraints, Solutions

2. Code for solving constraints

Requirements

In addition to the .cabal dependencies you require

• A Z3 (http://z3.codeplex.com) or CVC4 (http://cvc4.cs.nyu.edu) binary.