quickspec-0.9: Equational laws for free

Safe HaskellSafe-Inferred

Test.QuickSpec.Reasoning.CongruenceClosure

Description

A decision procedure for ground equality, based on the paper Proof-producing Congruence Closure.

Documentation

type CC = State SSource

newSym :: CC IntSource

(=:=) :: Int -> Int -> CC BoolSource

(=?=) :: Int -> Int -> CC BoolSource

rep :: Int -> CC IntSource

evalCC :: S -> CC a -> aSource

execCC :: S -> CC a -> SSource

runCC :: S -> CC a -> (a, S)Source

($$) :: Int -> Int -> CC IntSource

data S Source

funUse :: S -> IntMap [(Int, Int)]Source

argUse :: S -> IntMap [(Int, Int)]Source

lookup :: S -> IntMap (IntMap Int)Source

initial :: Int -> SSource

frozen :: CC a -> CC aSource