HaskHOL.Core

This module is the one to import for users looking to include the entirety of the core of the HaskHOL proof system. It re-exports all of the core sub-modules in addition to a number of overloaded functions that work with HOLTermRep and HOLTypeRep representations for convenience reasons.

HOLTermRep and HOLTypeRep Overloads

newConstant :: HOLTypeRep ty thry => String -> ty -> HOL Theory thry ()

A redefinition of newConstant to overload it for all valid term representations as defined by HOLTermRep.

newAxiom :: HOLTermRep tm thry => String -> tm -> HOL Theory thry HOLThm

A redefinition of newAxiom to overload it for all valid term representations as defined by HOLTermRep.

newBasicDefinition :: HOLTermRep tm thry => tm -> HOL Theory thry HOLThm

A redefinition of newBasicDefinition to overload it for all valid term representations as defined by HOLTermRep.

makeOverloadable :: HOLTypeRep ty thry => String -> ty -> HOL Theory thry ()

A redefinition of makeOverloadable to overload it for all valid type representations as defined by HOLTypeRep.

reduceInterface :: HOLTermRep tm thry => String -> tm -> HOL Theory thry ()

A redefinition of reduceInterface to overload it for all valid term representations as defined by HOLTermRep.

overrideInterface :: HOLTermRep tm thry => String -> tm -> HOL Theory thry ()

A redefinition of overrideInterface to overload it for all valid term representations as defined by HOLTermRep.

overloadInterface :: HOLTermRep tm thry => String -> tm -> HOL Theory thry ()

A redefinition of overloadInterface to overload it for all valid term representations as defined by HOLTermRep.

prioritizeOverload :: HOLTypeRep ty thry => ty -> HOL Theory thry ()

A redefinition of prioritizeOverload to overload it for all valid type representations as defined by HOLTypeRep.

newTypeAbbrev :: HOLTypeRep ty thry => String -> ty -> HOL Theory thry ()

A redefinition of newTypeAbbrev to overload it for all valid type representations as defined by HOLTypeRep.

Library and Utility Functions

module HaskHOL.Core.Lib

Logical Kernel

module HaskHOL.Core.Kernel

Stateful Primitives

module HaskHOL.Core.State

Basic Derived Type and Term Functions

module HaskHOL.Core.Basics

HaskHOL Parsers

module HaskHOL.Core.Parser

HaskHOL Pretty Printers

module HaskHOL.Core.Printer

HaskHOL Core Extensions

module HaskHOL.Core.Ext