type Validation d e = List d -> Eff (err :: Exception | e) dA Validation d e constructs a proof/derivation d from the proofs of its subgoals.
type ProofState j d e = { validation :: Validation d e, subgoals :: List j }A ProofState j d e is a list of subgoals (judgements j) and a validation.
newtype Tactic j d e
= Tactic (j -> Eff (err :: Exception | e) (ProofState j d e))A Tactic j d e is a strategy for constructing a proof in d of a judgement in j by transforming the proof state.
runTactic :: forall j d e. Tactic j d e -> j -> Eff (err :: Exception | e) (ProofState j d e)idT :: forall j d e. Tactic j d eThe identity tactic has no effect on the proof state.
lazyThenLT :: forall j d e. Tactic j d e -> Lazy [Tactic j d e] -> Tactic j d elazyThenLT t ts applies the tactics ts pointwise to the subgoals generated by the tactic t.
lazyThenT :: forall j d e. Tactic j d e -> Lazy (Tactic j d e) -> Tactic j d elazyThenT t1 t2 applies the tactic t2 to each of the subgoals generated by the tactic t.
thenLT :: forall j d e. Tactic j d e -> [Tactic j d e] -> Tactic j d ethenLT t ts applies the tactics ts pointwise to the subgoals generated by the tactic t.
thenT :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d ethenT t1 t2 applies the tactic t2 to each of the subgoals generated by the tactic t.
instance semigroupTactic :: Semigroup (Tactic j d e)Tactics form a semigroup via the thenT tactical.
instance monoidTactic :: Monoid (Tactic j d e)Tactics form a monoid via the idT tactic, which is the unit of thenT.
lazyOrElseT :: forall j d e. Tactic j d e -> Lazy (Tactic j d e) -> Tactic j d elazyOrElseT t1 t2first triest1, and if it fails, then tries t2`.
orElseT :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d eorElseT t1 t2first triest1, and if it fails, then tries t2`.
failT :: forall j d e. Tactic j d efailT always fails.
tryT :: forall j d e. Tactic j d e -> Tactic j d etryT either succeeds, or does nothing.
repeatT :: forall j d e. Tactic j d e -> Tactic j d erepeatT repeats a tactic for as long as it succeeds. repeatT never fails.
notT :: forall j d e. Tactic j d e -> Tactic j d eSucceeds if the tactic fails; fails if the tactic succeeds.
impliesT :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d eClassical "implication" of tactics: either the left tactic fails, or the right tactic succeeds. Note: I am not sure if this is useful at all, but it seemed interesting it was definable.
newtype AdditiveTactic j d e
= AdditiveTactic (Tactic j d e)The tactics also give rise to another semigroup and monoid structure, given by disjunction and failure.
getAdditiveTactic :: forall j d e. AdditiveTactic j d e -> Tactic j d einstance semigroupAdditiveTactic :: Semigroup (AdditiveTactic j d e)The semigroup operation is given by orElseT.
instance monoidAdditiveTactic :: Monoid (AdditiveTactic j d e)The monoid arises from the failT tactic, which is the unit of orElseT.
(/\) :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d eAn abbreviation for thenT.
(\/) :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d eAn abbreviation for orElseT.
(/\*) :: forall j d e. Tactic j d e -> [Tactic j d e] -> Tactic j d eAn abbreviation for thenLT.
(~>) :: forall j d e. Tactic j d e -> Tactic j d e -> Tactic j d eAn abbreviation for impliesT.