Data.Logic.Classes.Skolem

Documentation

class Variable v => Skolem f v | f -> v where

This class shows how to convert between atomic Skolem functions and Ints. We include a variable type as a parameter because we create skolem functions to replace an existentially quantified variable, and it can be helpful to retain a reference to the variable.

Methods

toSkolem :: v -> f

Built a Skolem function from the given variable and number. The number is generally obtained from the skolem monad.

isSkolem :: f -> Bool

Instances

Skolem Function String