| Copyright | (c) Artem Mavrin 2021 |
|---|---|
| License | BSD3 |
| Maintainer | artemvmavrin@gmail.com |
| Stability | experimental |
| Portability | POSIX |
| Safe Haskell | Safe |
| Language | Haskell2010 |
AutoProof.Internal.Judgement
Description
Defines the Judgement type and related functions.
Synopsis
- type Context a = Set (Formula a)
- data Judgement a = Judgement {
- antecedents :: Context a
- succedent :: Formula a
- (|-) :: (Ord a, Foldable f) => f (Formula a) -> Formula a -> Judgement a
- prettyJudgement :: PrettyPrintable a => Judgement a -> String
- weakenJudgement :: Ord a => Judgement a -> Formula a -> Judgement a
Types and constructors
type Context a = Set (Formula a) Source #
A set of propositional formulas, used as antecedents of a judgement.
(Judgement c a) represents the judgement or sequent \(c \vdash a\).
>>>Judgement Set.empty (Imp (And (Var 'a') (Var 'b')) (Var 'a'))[] |- Imp (And (Var 'a') (Var 'b')) (Var 'a')
Constructors
| Judgement | |
Fields
| |
Instances
| Eq a => Eq (Judgement a) Source # | |
| Ord a => Ord (Judgement a) Source # | |
Defined in AutoProof.Internal.Judgement | |
| (Ord a, Read a) => Read (Judgement a) Source # | |
| Show a => Show (Judgement a) Source # | |
| PrettyPrintable a => PrettyPrintable (Judgement a) Source # | |
(|-) :: (Ord a, Foldable f) => f (Formula a) -> Formula a -> Judgement a infix 5 Source #
Infix judgement constructor. (c represents the judgement
\(c \vdash a\).|- a)
>>>[Var 'a', Imp (Var 'a') (Var 'b')] |- Var 'b'[Var 'a',Imp (Var 'a') (Var 'b')] |- Var 'b'
Note: If c is already a Set, then it is recommended to use
(Judgement c a) in favor of (c , since the latter will create a
new set and fill it with the values in |- a)c.
Pretty-printing
prettyJudgement :: PrettyPrintable a => Judgement a -> String Source #
Get a pretty-printed representation of a judgement.
Examples
>>>prettyJudgement $ [Var "a", Imp (Var "a") (Var "b")] |- Var "b""a, a → b ⊢ b"