| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Zsyntax.Labelled.DerivationTerm
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.
Constructors
| 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 Methods 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 #