type-settheory-0.1.3.1: Sets and functions-as-relations in the type system

Type.Logic

Description

Propositions as types (of kind `*`), proofs as values

Synopsis

# Documentation

newtype Falsity Source

Constructors

 Falsity FieldselimFalsity :: forall a. a

Instances

 Typeable Falsity Decidable Falsity Typeable a => Show (a -> Falsity) Fact (Falsity -> a)

data Truth Source

Constructors

 TruthProof

Instances

 Show Truth Typeable Truth Decidable Truth Fact Truth

type Not a = a -> FalsitySource

class Fact a whereSource

This class collects lemmas. It plays no foundational role.

Methods

auto :: aSource

Instances

class Decidable a whereSource

Methods

decide :: Either (Not a) aSource

Instances

 Decidable Truth Decidable Falsity Finite s => Decidable (Ex s) Decidable a => Decidable (Not a) (Decidable a, Decidable b) => Decidable (a -> b) (Decidable a, Decidable b) => Decidable (Either a b) (Decidable a, Decidable b) => Decidable (a, b)

data Ex p whereSource

Existential quantification

Constructors

 Ex :: p b -> Ex p

Instances

 Finite s => Decidable (Ex s) Fact (p a) => Fact (Ex p) Fact (ExUniq p -> Ex p) Fact (Ex dom -> :==: (Const dom x) (Const dom' x') -> :=: x x')

exElim :: forall p r. (forall b. p b -> r) -> Ex p -> rSource

newtype All p Source

Universal quantification

Constructors

 All FieldsallElim :: forall b. p b

Instances

 Fact (All p -> p b)

data ExUniq p whereSource

Unique existence

Constructors

 ExUniq :: p b -> (forall b'. p b' -> b :=: b') -> ExUniq p

Instances

 Fact (ExUniq p -> p b -> p b' -> :=: b b') Fact (ExUniq p -> Ex p)

type COr r a b = Cont r (Either a b)Source

lem :: COr r (a -> r) aSource

elimCor :: COr r a b -> (a -> r) -> (b -> r) -> rSource

class Decidable1 s whereSource

Methods

decide1 :: Either (Not (s a)) (s a)Source

class Finite s whereSource

Methods

enum :: [Ex s]Source