jukebox-0.2.5: A first-order reasoning toolbox

Jukebox.GuessModel

data Universe Source #

Constructors

universe :: Universe -> Type -> NameM ([Function], [Form]) Source #

peano :: Type -> NameM ([Function], [Form]) Source #

trees :: Type -> NameM ([Function], [Form]) Source #

guessModel :: [String] -> Universe -> Problem Form -> Problem Form Source #

ind :: Symbolic a => a -> Type Source #

function :: [Function] -> Function -> Bool -> Function -> NameM [Form] Source #

rhss :: [Function] -> [Term] -> Function -> Bool -> Form -> [Form] Source #

cases :: [Function] -> [Type] -> NameM [[Term]] Source #

cases1 :: [Function] -> Type -> NameM [Term] Source #