hol-1.0: Higher order logic

LicenseMIT
MaintainerJoe Leslie-Hurd <joe@gilith.com>
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell98

HOL.Data

Description

 

Documentation

type Name = String Source #

data Type Source #

Constructors

Type TypeData Integer 

data TypeData Source #

Constructors

VarType TypeVar 
OpType TypeOp [Type] 

data TypeVar Source #

Constructors

TypeVar Name 

data TypeOp Source #

Constructors

TypeOp Name TypeOpProv 

data TypeOpProv Source #

Constructors

UndefTypeOpProv 
DefTypeOpProv TypeOpDef 

data TypeOpDef Source #

Constructors

TypeOpDef Term [TypeVar] 

data Var Source #

Constructors

Var Name Type 

data Term Source #

Constructors

Term TermData Type Integer 

data TermData Source #

Constructors

ConstTerm Const Type 
VarTerm Var 
AppTerm Term Term 
AbsTerm Var Term 

data Const Source #

Constructors

Const Name ConstProv 

data ConstProv Source #

Constructors

UndefConstProv 
DefConstProv ConstDef 
AbsConstProv TypeOp 
RepConstProv TypeOp 

data ConstDef Source #

Constructors

ConstDef Term