Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data DerivationTerm a l where
- Init :: a -> DerivationTerm a l
- Copy :: DerivationTerm a l -> LAxiom a l -> DerivationTerm a l
- ConjR :: DerivationTerm a l -> DerivationTerm a l -> l -> DerivationTerm a l
- ConjL :: DerivationTerm a l -> DerivationTerm a l
- ImplR :: DerivationTerm a l -> LFormula k a l -> ElemBase a -> ReactionList a -> l -> DerivationTerm a l
- ImplL :: DerivationTerm a l -> DerivationTerm a l -> LFormula k a l -> DerivationTerm a l
- concl :: DerivationTerm a l -> Opaque a l
- transitions :: DerivationTerm a l -> [(Opaque a l, Opaque a l)]
Documentation
data DerivationTerm a l where Source #
Derivation term of the labelled forward sequent calculus.
Init :: a -> DerivationTerm a l | |
Copy :: DerivationTerm a l -> LAxiom a l -> DerivationTerm a l | |
ConjR :: DerivationTerm a l -> DerivationTerm a l -> l -> DerivationTerm a l | |
ConjL :: DerivationTerm a l -> DerivationTerm a l | |
ImplR :: DerivationTerm a l -> LFormula k a l -> ElemBase a -> ReactionList a -> l -> DerivationTerm a l | |
ImplL :: DerivationTerm a l -> DerivationTerm a l -> LFormula k a l -> DerivationTerm a l |
Instances
Functor (DerivationTerm a) Source # | |
Defined in Zsyntax.Labelled.DerivationTerm fmap :: (a0 -> b) -> DerivationTerm a a0 -> DerivationTerm a b # (<$) :: a0 -> DerivationTerm a b -> DerivationTerm a a0 # |
concl :: DerivationTerm a l -> Opaque a l Source #
transitions :: DerivationTerm a l -> [(Opaque a l, Opaque a l)] Source #