| <!> | Refinery.Tactic |
| <@> | Refinery.Tactic |
| Alt | Refinery.Tactic |
| asRule | Refinery.Tactic.Internal |
| axiom | Refinery.ProofState |
| choice | Refinery.Tactic |
| focus | Refinery.Tactic |
| forSubgoals | Refinery.Tactic |
| goal | Refinery.Tactic |
| hole | Refinery.Tactic |
| many | Refinery.Tactic |
| many_ | Refinery.Tactic |
| mapExtract | Refinery.ProofState |
| mapRuleT | Refinery.Tactic.Internal |
| mapTacticT | Refinery.Tactic.Internal |
| MonadExtract | Refinery.Tactic |
| MonadProvable | Refinery.Tactic.Internal, Refinery.Tactic |
| MonadRule | Refinery.Tactic.Internal, Refinery.Tactic |
| progress | Refinery.Tactic |
| ProofStateT | |
| 1 (Type/Class) | Refinery.ProofState |
| 2 (Data Constructor) | Refinery.ProofState |
| Provable | Refinery.Tactic.Internal, Refinery.Tactic |
| ProvableT | |
| 1 (Type/Class) | Refinery.Tactic.Internal, Refinery.Tactic |
| 2 (Data Constructor) | Refinery.Tactic.Internal, Refinery.Tactic |
| proving | Refinery.Tactic.Internal, Refinery.Tactic |
| rule | Refinery.Tactic |
| RuleT | |
| 1 (Type/Class) | Refinery.Tactic.Internal, Refinery.Tactic |
| 2 (Data Constructor) | Refinery.Tactic.Internal |
| runProvable | Refinery.Tactic.Internal, Refinery.Tactic |
| runProvableT | Refinery.Tactic.Internal, Refinery.Tactic |
| runTacticT | Refinery.Tactic |
| some | Refinery.Tactic |
| stateful | Refinery.Tactic.Internal |
| subgoal | Refinery.Tactic.Internal, Refinery.Tactic |
| TacticT | |
| 1 (Type/Class) | Refinery.Tactic.Internal, Refinery.Tactic |
| 2 (Data Constructor) | Refinery.Tactic.Internal |
| try | Refinery.Tactic |
| unProofStateT | Refinery.ProofState |
| unRuleT | Refinery.Tactic.Internal |
| unTacticT | Refinery.Tactic.Internal |