| And | AutoProof.Internal.Formula.Types, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| AndElimL | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| andElimLS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| AndElimR | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| andElimRS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| AndIntr | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| andIntrS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| andS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| antecedents | AutoProof.Internal.Judgement, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| anyChar | AutoProof.Internal.Utils.Parser.Char, AutoProof.Internal.Utils.Parser |
| AST | AutoProof.Internal.AST, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| ASTMetadata | |
| 1 (Type/Class) | AutoProof.Internal.AST |
| 2 (Data Constructor) | AutoProof.Internal.AST |
| atomicASTConstructor | AutoProof.Internal.AST |
| Axiom | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| axiomS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| between | AutoProof.Internal.Utils.Parser.Combinator, AutoProof.Internal.Utils.Parser |
| binaryASTConstructor | AutoProof.Internal.AST |
| binaryRootedASTConstructor | AutoProof.Internal.AST |
| branchS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| canonicalCNF | AutoProof.Internal.Classical.CNF, AutoProof.Classical.CNF, AutoProof.Classical |
| chainl1 | AutoProof.Internal.Utils.Parser.Combinator, AutoProof.Internal.Utils.Parser |
| chainr1 | AutoProof.Internal.Utils.Parser.Combinator, AutoProof.Internal.Utils.Parser |
| char | AutoProof.Internal.Utils.Parser.Char, AutoProof.Internal.Utils.Parser |
| charIf | AutoProof.Internal.Utils.Parser.Char, AutoProof.Internal.Utils.Parser |
| children | AutoProof.Internal.AST, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| Clause | AutoProof.Internal.Classical.CNF, AutoProof.Classical.CNF |
| CNF | AutoProof.Internal.Classical.CNF, AutoProof.Classical.CNF |
| cons | AutoProof.Internal.Utils.DList |
| Context | AutoProof.Internal.Judgement, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| cornerS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| correct | AutoProof.Internal.Intuitionistic.Proof.Correctness, AutoProof.Internal.Intuitionistic.Proof, AutoProof.Intuitionistic |
| debug | AutoProof.Internal.Intuitionistic.Proof.Correctness, AutoProof.Internal.Intuitionistic.Proof, AutoProof.Intuitionistic |
| DList | AutoProof.Internal.Utils.DList |
| empty | AutoProof.Internal.Utils.DList |
| eof | AutoProof.Internal.Utils.Parser.Combinator, AutoProof.Internal.Utils.Parser |
| evalFormula | AutoProof.Internal.Classical.SAT.TruthAssignment, AutoProof.Internal.Classical.SAT, AutoProof.Classical |
| evalVar | AutoProof.Internal.Classical.SAT.TruthAssignment, AutoProof.Internal.Classical.SAT, AutoProof.Classical |
| FalseElim | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| falseElimS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| falseS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| findCut | AutoProof.Internal.Intuitionistic.Proof.Cut, AutoProof.Internal.Intuitionistic.Proof, AutoProof.Intuitionistic |
| Formula | AutoProof.Internal.Formula.Types, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| fromFormula | AutoProof.Internal.Classical.CNF, AutoProof.Classical.CNF |
| fromList | AutoProof.Internal.Utils.DList |
| getAnyLiteral | AutoProof.Internal.Classical.CNF, AutoProof.Classical.CNF |
| getAnyVariable | AutoProof.Internal.Formula.Operations, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| getHeight | AutoProof.Internal.AST |
| getSize | AutoProof.Internal.AST |
| glivenkoTranslate | AutoProof.Internal.Classical.Proof.Glivenko |
| hasCut | AutoProof.Internal.Intuitionistic.Proof.Cut, AutoProof.Internal.Intuitionistic.Proof, AutoProof.Intuitionistic |
| height | AutoProof.Internal.AST, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| Iff | AutoProof.Internal.Formula.Types, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| IffElimL | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| iffElimLS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| IffElimR | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| iffElimRS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| IffIntr | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| iffIntrS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| iffS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| Imp | AutoProof.Internal.Formula.Types, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| ImpElim | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| impElimS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| ImpIntr | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| impIntrS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| impS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| isProvable | |
| 1 (Function) | AutoProof.Internal.Intuitionistic.Proof.Provability, AutoProof.Internal.Intuitionistic.Proof, AutoProof.Intuitionistic |
| 2 (Function) | AutoProof.Internal.Classical.Proof.Provability, AutoProof.Internal.Classical.Proof, AutoProof.Classical |
| isProvableGlivenko | AutoProof.Internal.Classical.Proof.Glivenko |
| isTautology | |
| 1 (Function) | AutoProof.Internal.Intuitionistic.Proof.Provability, AutoProof.Internal.Intuitionistic.Proof, AutoProof.Intuitionistic |
| 2 (Function) | AutoProof.Internal.Classical.Proof.Provability, AutoProof.Internal.Classical.Proof, AutoProof.Classical |
| Judgement | |
| 1 (Type/Class) | AutoProof.Internal.Judgement, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| 2 (Data Constructor) | AutoProof.Internal.Judgement, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| Lit | AutoProof.Internal.Formula.Types, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| Literal | AutoProof.Internal.Classical.CNF, AutoProof.Classical.CNF |
| metadata | AutoProof.Internal.AST |
| Not | AutoProof.Internal.Formula.Types, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| NotElim | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| notElimS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| notFollowedBy | AutoProof.Internal.Utils.Parser.Combinator, AutoProof.Internal.Utils.Parser |
| NotIntr | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| notIntrS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| notS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| oneOf | AutoProof.Internal.Utils.Parser.Char, AutoProof.Internal.Utils.Parser |
| Or | AutoProof.Internal.Formula.Types, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| OrElim | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| orElimS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| OrIntrL | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| orIntrLS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| OrIntrR | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| orIntrRS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| orS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| parse | AutoProof.Internal.Utils.Parser.Types, AutoProof.Internal.Utils.Parser |
| parseFormula | AutoProof.Internal.Parser, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| parseJudgement | AutoProof.Internal.Parser, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| Parser | |
| 1 (Type/Class) | AutoProof.Internal.Utils.Parser.Types, AutoProof.Internal.Utils.Parser |
| 2 (Data Constructor) | AutoProof.Internal.Utils.Parser.Types |
| pretty | AutoProof.Internal.Utils.PrettyPrintable, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| prettyFormula | AutoProof.Internal.Formula.Types, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| prettyJudgement | AutoProof.Internal.Judgement, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| PrettyPrintable | AutoProof.Internal.Utils.PrettyPrintable |
| prettyProof | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| prettys | AutoProof.Internal.Utils.PrettyPrintable |
| prettySeq | AutoProof.Internal.Utils.PrettyPrintable |
| prettysSeq | AutoProof.Internal.Utils.PrettyPrintable |
| Proof | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| properSubtrees | AutoProof.Internal.AST, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| prove | AutoProof.Internal.Intuitionistic.Proof.Search.General, AutoProof.Internal.Intuitionistic.Proof.Search, AutoProof.Internal.Intuitionistic.Proof, AutoProof.Intuitionistic |
| proveImp | AutoProof.Internal.Intuitionistic.Proof.Search.Implication, AutoProof.Internal.Intuitionistic.Proof.Search, AutoProof.Internal.Intuitionistic.Proof, AutoProof.Intuitionistic |
| proveStatman | AutoProof.Internal.Intuitionistic.Proof.Search.Statman, AutoProof.Internal.Intuitionistic.Proof.Search, AutoProof.Internal.Intuitionistic.Proof, AutoProof.Intuitionistic |
| proveTautology | AutoProof.Internal.Intuitionistic.Proof.Search.General, AutoProof.Internal.Intuitionistic.Proof.Search, AutoProof.Internal.Intuitionistic.Proof, AutoProof.Intuitionistic |
| pureLiteral | AutoProof.Internal.Classical.CNF, AutoProof.Classical.CNF |
| Root | AutoProof.Internal.AST, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| root | AutoProof.Internal.AST, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| runParser | AutoProof.Internal.Utils.Parser.Types |
| satAssignmentDPLL | AutoProof.Internal.Classical.SAT.Algorithms.DPLL, AutoProof.Internal.Classical.SAT.Algorithms, AutoProof.Internal.Classical.SAT, AutoProof.Classical |
| satAssignmentSimple | AutoProof.Internal.Classical.SAT.Algorithms.Simple, AutoProof.Internal.Classical.SAT.Algorithms, AutoProof.Internal.Classical.SAT, AutoProof.Classical |
| satDPLL | AutoProof.Internal.Classical.SAT.Algorithms.DPLL, AutoProof.Internal.Classical.SAT.Algorithms, AutoProof.Internal.Classical.SAT, AutoProof.Classical |
| satSimple | AutoProof.Internal.Classical.SAT.Algorithms.Simple, AutoProof.Internal.Classical.SAT.Algorithms, AutoProof.Internal.Classical.SAT, AutoProof.Classical |
| sepBy | AutoProof.Internal.Utils.Parser.Combinator, AutoProof.Internal.Utils.Parser |
| sepBy1 | AutoProof.Internal.Utils.Parser.Combinator, AutoProof.Internal.Utils.Parser |
| singleton | AutoProof.Internal.Utils.DList |
| size | AutoProof.Internal.AST, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| spaces | AutoProof.Internal.Utils.Parser.Char, AutoProof.Internal.Utils.Parser |
| strengthenProof | AutoProof.Internal.Proof.Structural, AutoProof.Internal.Proof |
| string | AutoProof.Internal.Utils.Parser.Char, AutoProof.Internal.Utils.Parser |
| subformulas | AutoProof.Internal.Formula.Operations, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| substitute | |
| 1 (Function) | AutoProof.Internal.Formula.Operations, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| 2 (Function) | AutoProof.Internal.Classical.CNF, AutoProof.Classical.CNF |
| substitutePure | AutoProof.Internal.Classical.CNF, AutoProof.Classical.CNF |
| subtrees | AutoProof.Internal.AST, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| succedent | AutoProof.Internal.Judgement, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| ternaryRootedASTConstructor | AutoProof.Internal.AST |
| toFormula | AutoProof.Internal.Classical.CNF, AutoProof.Classical.CNF |
| toImp | AutoProof.Internal.Intuitionistic.Proof.Search.Statman |
| toList | AutoProof.Internal.Utils.DList |
| toMap | AutoProof.Internal.Utils.MapUtils |
| toSet | |
| 1 (Function) | AutoProof.Internal.Utils.DList |
| 2 (Function) | AutoProof.Internal.Utils.SetUtils |
| TrueIntr | AutoProof.Internal.Proof.Types, AutoProof.Internal.Proof, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| trueIntrS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| trueS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| TruthAssignment | AutoProof.Internal.Classical.SAT.TruthAssignment, AutoProof.Internal.Classical.SAT, AutoProof.Classical |
| turnstileS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| unaryASTConstructor | AutoProof.Internal.AST |
| unaryRootedASTConstructor | AutoProof.Internal.AST |
| unitLiteral | AutoProof.Internal.Classical.CNF, AutoProof.Classical.CNF |
| unsafeParseFormula | AutoProof.Internal.Parser |
| unsafeParseJudgement | AutoProof.Internal.Parser |
| valid | AutoProof.Internal.Intuitionistic.Proof.Correctness, AutoProof.Internal.Intuitionistic.Proof, AutoProof.Intuitionistic |
| Var | AutoProof.Internal.Formula.Types, AutoProof.Internal.Formula, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| vertS | AutoProof.Internal.Utils.PrettyPrintable.Symbols |
| weakenJudgement | AutoProof.Internal.Judgement, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| weakenProof | AutoProof.Internal.Proof.Structural, AutoProof.Internal.Proof |
| |- | AutoProof.Internal.Judgement, AutoProof.Classical, AutoProof, AutoProof.Intuitionistic |
| |= | AutoProof.Internal.Classical.SAT.TruthAssignment, AutoProof.Internal.Classical.SAT, AutoProof.Classical |