| <%> | Refinery.Tactic |
| <@> | Refinery.Tactic |
| Alt | Refinery.ProofState |
| attempt | Refinery.Tactic |
| Axiom | Refinery.ProofState |
| choice | Refinery.Tactic |
| Commit | Refinery.ProofState |
| commit | Refinery.Tactic |
| DependentMetaSubst | Refinery.ProofState, Refinery.Tactic |
| dependentSubst | Refinery.ProofState, Refinery.Tactic |
| Effect | Refinery.ProofState |
| Empty | Refinery.ProofState |
| ensure | Refinery.Tactic |
| evalTacticT | Refinery.Tactic |
| Failure | Refinery.ProofState |
| failure | Refinery.Tactic |
| focus | Refinery.Tactic |
| goal | Refinery.Tactic |
| Handle | Refinery.ProofState |
| handler | Refinery.Tactic |
| handler_ | Refinery.Tactic |
| hole | Refinery.ProofState, Refinery.Tactic |
| inspect | Refinery.Tactic |
| Interleave | Refinery.ProofState |
| many_ | Refinery.Tactic |
| mapExtract | Refinery.ProofState |
| mapTacticT | Refinery.Tactic.Internal |
| MetaSubst | Refinery.ProofState, Refinery.Tactic |
| MonadExtract | Refinery.ProofState, Refinery.Tactic |
| PartialProof | |
| 1 (Type/Class) | Refinery.ProofState, Refinery.Tactic |
| 2 (Data Constructor) | Refinery.ProofState, Refinery.Tactic |
| partialProofs | Refinery.ProofState |
| peek | Refinery.Tactic |
| pf_extract | Refinery.ProofState, Refinery.Tactic |
| pf_state | Refinery.ProofState, Refinery.Tactic |
| pf_unsolvedGoals | Refinery.ProofState, Refinery.Tactic |
| progress | Refinery.Tactic |
| Proof | |
| 1 (Type/Class) | Refinery.ProofState, Refinery.Tactic |
| 2 (Data Constructor) | Refinery.ProofState, Refinery.Tactic |
| proofs | Refinery.ProofState |
| proofState | Refinery.Tactic.Internal |
| ProofStateT | Refinery.ProofState |
| proofState_ | Refinery.Tactic.Internal |
| pruning | Refinery.Tactic |
| reify | Refinery.Tactic |
| resume | Refinery.Tactic |
| resume' | Refinery.Tactic |
| rule | Refinery.Tactic |
| RuleT | |
| 1 (Type/Class) | Refinery.Tactic.Internal, Refinery.Tactic |
| 2 (Data Constructor) | Refinery.Tactic.Internal |
| rule_ | Refinery.Tactic |
| runPartialTacticT | Refinery.Tactic |
| runTacticT | Refinery.Tactic |
| some_ | Refinery.Tactic |
| speculate | Refinery.ProofState |
| Stateful | Refinery.ProofState |
| Subgoal | Refinery.ProofState |
| subgoal | Refinery.Tactic.Internal, Refinery.Tactic |
| subgoals | Refinery.ProofState |
| substMeta | Refinery.ProofState, Refinery.Tactic |
| tactic | Refinery.Tactic.Internal |
| TacticT | |
| 1 (Type/Class) | Refinery.Tactic.Internal, Refinery.Tactic |
| 2 (Data Constructor) | Refinery.Tactic.Internal |
| try | Refinery.Tactic |
| tweak | Refinery.Tactic |
| unRuleT | Refinery.Tactic.Internal |
| unsolvable | Refinery.Tactic.Internal, Refinery.Tactic |
| unsolvableHole | Refinery.ProofState, Refinery.Tactic |
| unTacticT | Refinery.Tactic.Internal |