Hets - the Heterogeneous Tool Set

Copyright(c) Christian Maeder, Uni Bremen 2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

CASL.AlphaConvert

Description

uniquely rename variables in quantified formulas to allow for a formula equality modulo alpha conversion

Synopsis

Documentation

alphaEquiv :: Eq f => (f -> f) -> FORMULA f -> FORMULA f -> Bool

formula equality modulo alpha conversion

convertFormula :: Int -> (f -> f) -> FORMULA f -> FORMULA f

uniquely rename variables in quantified formulas and always quantify only over a single variable

alphaConvert :: Int -> (f -> f) -> FORMULA f -> (FORMULA f, Int)