theoremquest-0.0.0: A common library for TheoremQuest, a theorem proving game.

TheoremQuest.Logic

Synopsis

Documentation

data Term Source

Constructors

Const String Type
Var Variable
Abs Variable Term
Comb Term Term

Instances

Eq Term
Read Term
Show Term
JSON Term
TypeOf Term

type Proposition = Term Source

A boolean term.

data Variable Source

Constructors

Variable String Type

Instances

Eq Variable
Read Variable
Show Variable
TypeOf Variable

data Theorem Source

data Type Source

Constructors

Bool
Type :-> Type

Instances

Eq Type
Read Type
Show Type
TypeOf Type

data Inference a Source

Constructors

REFL Term
TRANS a a
MK_COMB a a
ABS Term a
BETA Term
ASSUME Term
EQ_MP a a
DEDUCT_ANTISYM a a
INST [(Variable, Term)] a
INST_TYPE [(Type, Type)] a
AXIOM Axiom

Instances

Read a => Read (Inference a)
Show a => Show (Inference a)

data Axiom Source

Constructors

Instances

Read Axiom
Show Axiom

class TypeOf a whereSource

Methods

typeOf :: a -> Type Source

Instances

TypeOf Type
TypeOf Variable
TypeOf Term

(=.) :: Term -> Term -> Term Source

assumptions :: Theorem -> [Proposition]Source

Assumptions of a Theorem.

conclusion :: Theorem -> Proposition Source

Conclusion of a Theorem.

inference :: Inference Theorem -> Maybe Theorem Source

Creates a Theorem from an Inference rule application.

wellTyped :: Term -> Bool Source

Checks if a term is well-typed.

freeIn :: Variable -> Term -> Bool Source

Checks if a variable is free in a term.

freeVariables :: Term -> [Variable]Source

All free variables in a term.