All Versions
15
Latest Version
Avg Release Cycle
135 days
Latest Release
-

Changelog History
Page 1

  • v0.8.0.1 Changes

    • 👌 Support for HORN-NNF format clauses, see tests/horn/{pos,neg}/*.smt2
    • 👌 Support for "existential binders", see tests/pos/ebind-*.fq for example. This only works with --eliminate.
    • 🚚 Move to GHC 8.4.3

  • v0.7.0.7 Changes

    February 15, 2018

    ➕ Add support for coercions to support GADTs.

  • v0.7.0.1 Changes

    August 24, 2017

    Many changes and new features, including:

    👀 1. New eliminate based solver (see ICFP 2017 paper for algorithm) 👀 2. Proof by Logical Evaluation see tests/proof

    1. SMTLIB2 ADTs to make data constructors injective 👍 4. Uniformly support polymorphic functions via elaborate

  • v0.7.0.0 Changes

    • 🆕 New eliminate based solver (see ICFP 2017 paper for algorithm)
    • 👀 Proof by Logical Evaluation see tests/proof
    • SMTLIB2 ADTs to make data constructors injective
    • 👍 Uniformly support polymorphic functions via apply and elaborate

  • v0.5.0.1

    April 05, 2016

  • v0.5.0.0

    April 01, 2016

  • v0.4.0.0

    August 12, 2015

  • v0.3.0.1

    May 22, 2015

  • v0.3.0.0 Changes

    • 0️⃣ Make interpreted mul and div the default, when solver = z3
    • 👉 Use higherorder flag to allow higher order binders into the environment

  • v0.2.3.2

    March 27, 2015