Type.Logic
Description
Propositions as types (of kind *), proofs as values
Synopsis
newtype Falsity = Falsity {
 elimFalsity :: forall a. a
}
data Truth = TruthProof
type Not a = a -> Falsity
class Fact a where
 auto :: a
data Decidable a = Decidable {
 decide :: Either (Not a) a
}
data Ex p where
 Ex :: p b -> Ex p
exElim :: forall p r. (forall b. p b -> r) -> Ex p -> r
newtype All p = All {
 allElim :: forall b. p b
}
data ExUniq p where
 ExUniq :: p b -> (forall b'. p b' -> b :=: b') -> ExUniq p
type COr r a b = Cont r (Either a b)
lem :: COr r (a -> r) a
elimCor :: COr r a b -> (a -> r) -> (b -> r) -> r
Documentation
 newtype Falsity Source
Constructors
Falsity
 elimFalsity :: forall a. a
Instances
 Show Falsity Typeable Falsity
 data Truth Source
Constructors
 TruthProof
Instances
 Show Truth Typeable Truth Fact Truth
 type Not a = a -> Falsity Source
 class Fact a where Source
This class collects lemmas. It plays no foundational role.
Methods
 auto :: a Source
Instances
 data Decidable a Source
Constructors
Decidable
 decide :: Either (Not a) a
Instances
 Typeable1 Decidable (Show a, Typeable a) => Show (Decidable a) Fact (Decidable Truth) Fact (Decidable Falsity)
 data Ex p where Source
Existential quantification
Constructors
 Ex :: p b -> Ex p
Instances
 Fact (p a) => Fact (Ex p)
 exElim :: forall p r. (forall b. p b -> r) -> Ex p -> r Source
 newtype All p Source
Universal quantification
Constructors
All
 allElim :: forall b. p b
 data ExUniq p where Source
Unique existence
Constructors
 ExUniq :: p b -> (forall b'. p b' -> b :=: b') -> ExUniq p
 type COr r a b = Cont r (Either a b) Source
 lem :: COr r (a -> r) a Source
 elimCor :: COr r a b -> (a -> r) -> (b -> r) -> r Source