refinery

Please see the README on GitHub at https://github.com/githubuser/refinery#readme


Keywords
language, library, Propose Tags , Refinery.ProofState, Refinery.Tactic, Refinery.Tactic.Internal, Algebraic Foundations of Proof Refinement, metaprogramming, proof-automation, proof-refinement
License
BSD-3-Clause
Install
cabal install refinery

Documentation

refinery

refinery is a toolkit for building proof refinement/proof automation systems, based roughly on the Algebraic Foundations of Proof Refinement.

Overview

The main datatype of the library is TacticT goal extract m a, which is a monad transformer that behaves as a tactic. When creating your domain-specific tactics, you should use RuleT and rule to implement them.