Index
| :!=: | Data.TSTP |
| :&: | Data.TSTP |
| :<=: | Data.TSTP |
| :<=>: | Data.TSTP |
| :<~>: | Data.TSTP |
| :=: | Data.TSTP |
| :=>: | Data.TSTP |
| :|: | Data.TSTP |
| :~&: | Data.TSTP |
| :~: | Data.TSTP |
| :~|: | Data.TSTP |
| AC | Data.TSTP |
| agdafy | Util |
| AgdaSignature | T2A.Core |
| All | Data.TSTP |
| Assumption | Data.TSTP |
| AssumptionR | Data.TSTP |
| Assumption_ | Data.TSTP |
| AtomicWord | |
| 1 (Type/Class) | Data.TSTP |
| 2 (Data Constructor) | Data.TSTP |
| Axiom | Data.TSTP |
| AxiomOfChoice | Data.TSTP |
| BinOp | |
| 1 (Type/Class) | Data.TSTP |
| 2 (Data Constructor) | Data.TSTP |
| bottom | Data.TSTP |
| BShow | Util |
| buildProofMap | Data.Proof, T2A |
| buildProofTree | Data.Proof, T2A |
| buildSignature | T2A.Core |
| Canonicalize | Data.TSTP |
| Cax | Data.TSTP |
| Ceq | Data.TSTP |
| checkIdScope | Util |
| ColonSep | Data.TSTP |
| Conjecture | Data.TSTP |
| Creator | Data.TSTP |
| Csa | Data.TSTP |
| Csp | Data.TSTP |
| Cth | Data.TSTP |
| Cup | Data.TSTP |
| Definition | Data.TSTP |
| Definition_ | Data.TSTP |
| Description | Data.TSTP |
| DistinctObjectTerm | Data.TSTP |
| Ecs | Data.TSTP |
| Ect | Data.TSTP |
| Equality | Data.TSTP |
| Eqv | Data.TSTP |
| Esa | Data.TSTP |
| Eth | Data.TSTP |
| Exists | Data.TSTP |
| F | |
| 1 (Type/Class) | Data.TSTP |
| 2 (Data Constructor) | Data.TSTP |
| FiDomain | Data.TSTP |
| FiFunctors | Data.TSTP |
| File | Data.TSTP |
| FiPredicates | Data.TSTP |
| fname | T2A.Core |
| Formula | Data.TSTP |
| formula | Data.TSTP |
| freeVarsF | Data.TSTP |
| freeVarsT | Data.TSTP |
| Fsa | Data.TSTP |
| Fun | Data.TSTP |
| FunApp | Data.TSTP |
| Function | Data.TSTP |
| GApp | Data.TSTP |
| GData | Data.TSTP |
| GDistinctObject | Data.TSTP |
| getAxioms | T2A |
| getConjeture | T2A |
| getFreeVars | Data.TSTP |
| getParents | Data.Proof |
| getParentsTree | Data.Proof |
| getRefutes | T2A |
| getSubGoals | T2A |
| GFormulaData | Data.TSTP |
| GFormulaTerm | Data.TSTP |
| GList | Data.TSTP |
| GNumber | Data.TSTP |
| GTerm | |
| 1 (Type/Class) | Data.TSTP |
| 2 (Data Constructor) | Data.TSTP |
| GVar | Data.TSTP |
| GWord | Data.TSTP |
| Hypothesis | Data.TSTP |
| identity | T2A.Tactics |
| IdSet | Data.Proof |
| Inference | Data.TSTP |
| InferenceInfo | Data.TSTP |
| InfixPred | |
| 1 (Type/Class) | Data.TSTP |
| 2 (Data Constructor) | Data.TSTP |
| Info | Data.TSTP |
| Introduced | Data.TSTP |
| IntroType | Data.TSTP |
| IQuote | Data.TSTP |
| isBottom | Data.TSTP |
| Leaf | Data.Proof |
| Lemma | Data.TSTP |
| Name | Data.TSTP |
| name | Data.TSTP |
| Negate | Data.TSTP |
| NegatedConjecture | Data.TSTP |
| NewRule | Data.TSTP |
| Noc | Data.TSTP |
| NoSource | Data.TSTP |
| NumberLitTerm | Data.TSTP |
| Parent | |
| 1 (Type/Class) | Data.TSTP |
| 2 (Data Constructor) | Data.TSTP |
| parse | TSTP |
| parseFile | TSTP, T2A |
| Plain | Data.TSTP |
| PredApp | Data.TSTP |
| printAuxSignatures | T2A |
| printInd | Util |
| printPreamble | T2A |
| printProofBody | T2A |
| printProofWhere | T2A |
| printSubGoals | T2A |
| ProofMap | Data.Proof |
| ProofTree | Data.Proof |
| ProofTreeGen | Data.Proof |
| putStrLnInd | Util |
| Quant | |
| 1 (Type/Class) | Data.TSTP |
| 2 (Data Constructor) | Data.TSTP |
| Refutation | Data.TSTP |
| resolveTactic | T2A.Tactics |
| resolveTacticGen | T2A.Tactics |
| Role | Data.TSTP |
| role | Data.TSTP |
| Root | Data.Proof |
| Rule | Data.TSTP |
| Sap | Data.TSTP |
| Sat | Data.TSTP |
| Sca | Data.TSTP |
| Scc | Data.TSTP |
| ScopedSignature | T2A.Core |
| Signature | T2A.Core |
| Simplify | Data.TSTP |
| Source | |
| 1 (Type/Class) | Data.TSTP |
| 2 (Data Constructor) | Data.TSTP |
| source | Data.TSTP |
| Status | |
| 1 (Type/Class) | Data.TSTP |
| 2 (Data Constructor) | Data.TSTP |
| stdout2file | Util |
| Strip | Data.TSTP |
| Suc | Data.TSTP |
| swapPrefix | Util |
| Tac | Data.TSTP |
| Tactic | T2A.Tactics |
| Tau | Data.TSTP |
| Tautology | Data.TSTP |
| Tca | Data.TSTP |
| Term | Data.TSTP |
| Theorem | Data.TSTP |
| Theory | |
| 1 (Type/Class) | Data.TSTP |
| 2 (Data Constructor) | Data.TSTP |
| Thm | Data.TSTP |
| Type | Data.TSTP |
| Uca | Data.TSTP |
| Unc | Data.TSTP |
| unique | Util |
| Unk | Data.TSTP |
| Unknown | Data.TSTP |
| unknownTree | Data.Proof |
| UnknownType | Data.TSTP |
| Unp | Data.TSTP |
| Uns | Data.TSTP |
| V | |
| 1 (Type/Class) | Data.TSTP |
| 2 (Data Constructor) | Data.TSTP |
| Var | Data.TSTP |
| Wca | Data.TSTP |
| Wcc | Data.TSTP |
| Wct | Data.TSTP |
| Wec | Data.TSTP |
| Wtc | Data.TSTP |
| Wth | Data.TSTP |
| Wuc | Data.TSTP |
| βshow | Util |
| ▪ | Util |