Index
| Action | Copilot.Theorem.Prove |
| Admit | Copilot.Theorem.Prove |
| admit | Copilot.Theorem |
| altErgo | Copilot.Theorem.Prover.SMT |
| askProver | Copilot.Theorem.Prove |
| Assume | Copilot.Theorem.Prove |
| assume | Copilot.Theorem |
| Backend | Copilot.Theorem.Prover.SMT |
| bmcMax | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
| Bool | Copilot.Theorem.Kind2 |
| Check | Copilot.Theorem.Prove |
| check | Copilot.Theorem.Prove |
| closeProver | Copilot.Theorem.Prove |
| combine | Copilot.Theorem.Prove |
| cvc4 | Copilot.Theorem.Prover.SMT |
| debug | |
| 1 (Function) | Copilot.Theorem.Prover.SMT |
| 2 (Function) | Copilot.Theorem.Prover.Z3 |
| def | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2, Copilot.Theorem.Prover.SMT, Copilot.Theorem.Prover.Z3 |
| Default | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2, Copilot.Theorem.Prover.SMT, Copilot.Theorem.Prover.Z3 |
| dReal | Copilot.Theorem.Prover.SMT |
| Error | Copilot.Theorem.Prove |
| Existential | Copilot.Theorem.Prove, Copilot.Theorem |
| FConst | Copilot.Theorem.Kind2 |
| File | |
| 1 (Type/Class) | Copilot.Theorem.Kind2 |
| 2 (Data Constructor) | Copilot.Theorem.Kind2 |
| filePreds | Copilot.Theorem.Kind2 |
| fileProps | Copilot.Theorem.Kind2 |
| FunApp | Copilot.Theorem.Kind2 |
| induction | |
| 1 (Function) | Copilot.Theorem.Prover.SMT |
| 2 (Function) | Copilot.Theorem.Prover.Z3 |
| Init | Copilot.Theorem.Kind2 |
| Inlined | Copilot.Theorem.Kind2 |
| instantiate | Copilot.Theorem |
| Int | Copilot.Theorem.Kind2 |
| Invalid | Copilot.Theorem.Prove |
| kind2Prover | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
| kInduction | |
| 1 (Function) | Copilot.Theorem.Prover.SMT |
| 2 (Function) | Copilot.Theorem.Prover.Z3 |
| mathsat | Copilot.Theorem.Prover.SMT |
| maxK | |
| 1 (Function) | Copilot.Theorem.Prover.SMT |
| 2 (Function) | Copilot.Theorem.Prover.Z3 |
| metit | Copilot.Theorem.Prover.SMT |
| Modular | Copilot.Theorem.Kind2 |
| nraNLSat | Copilot.Theorem.Prover.Z3 |
| onlySat | |
| 1 (Function) | Copilot.Theorem.Prover.SMT |
| 2 (Function) | Copilot.Theorem.Prover.Z3 |
| onlyValidity | |
| 1 (Function) | Copilot.Theorem.Prover.SMT |
| 2 (Function) | Copilot.Theorem.Prover.Z3 |
| Options | |
| 1 (Type/Class) | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
| 2 (Data Constructor) | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
| 3 (Type/Class) | Copilot.Theorem.Prover.SMT |
| 4 (Data Constructor) | Copilot.Theorem.Prover.SMT |
| 5 (Type/Class) | Copilot.Theorem.Prover.Z3 |
| 6 (Data Constructor) | Copilot.Theorem.Prover.Z3 |
| Output | |
| 1 (Type/Class) | Copilot.Theorem.Prove |
| 2 (Data Constructor) | Copilot.Theorem.Prove |
| PredApp | Copilot.Theorem.Kind2 |
| PredDef | |
| 1 (Type/Class) | Copilot.Theorem.Kind2 |
| 2 (Data Constructor) | Copilot.Theorem.Kind2 |
| predId | Copilot.Theorem.Kind2 |
| predInit | Copilot.Theorem.Kind2 |
| predStateVars | Copilot.Theorem.Kind2 |
| predTrans | Copilot.Theorem.Kind2 |
| PredType | Copilot.Theorem.Kind2 |
| prettyPrint | Copilot.Theorem.Kind2 |
| PrimedStateVar | Copilot.Theorem.Kind2 |
| Proof | |
| 1 (Data Constructor) | Copilot.Theorem.Prove |
| 2 (Type/Class) | Copilot.Theorem.Prove, Copilot.Theorem |
| ProofScheme | Copilot.Theorem.Prove |
| Prop | |
| 1 (Type/Class) | Copilot.Theorem.Kind2 |
| 2 (Data Constructor) | Copilot.Theorem.Kind2 |
| PropId | Copilot.Theorem.Prove, Copilot.Theorem |
| propName | Copilot.Theorem.Kind2 |
| PropRef | |
| 1 (Type/Class) | Copilot.Theorem.Prove, Copilot.Theorem |
| 2 (Data Constructor) | Copilot.Theorem.Prove |
| propTerm | Copilot.Theorem.Kind2 |
| prove | Copilot.Theorem.Prove |
| Prover | |
| 1 (Type/Class) | Copilot.Theorem.Prove |
| 2 (Data Constructor) | Copilot.Theorem.Prove |
| proverName | Copilot.Theorem.Prove |
| Real | Copilot.Theorem.Kind2 |
| Sat | Copilot.Theorem.Prove |
| SmtFormat | Copilot.Theorem.Prover.SMT |
| SmtLib | Copilot.Theorem.Prover.SMT |
| startK | |
| 1 (Function) | Copilot.Theorem.Prover.SMT |
| 2 (Function) | Copilot.Theorem.Prover.Z3 |
| startProver | Copilot.Theorem.Prove |
| StateVar | Copilot.Theorem.Kind2 |
| StateVarDef | |
| 1 (Type/Class) | Copilot.Theorem.Kind2 |
| 2 (Data Constructor) | Copilot.Theorem.Kind2 |
| StateVarFlag | Copilot.Theorem.Kind2 |
| Status | Copilot.Theorem.Prove |
| Style | Copilot.Theorem.Kind2 |
| Term | Copilot.Theorem.Kind2 |
| toKind2 | Copilot.Theorem.Kind2 |
| Tptp | Copilot.Theorem.Prover.SMT |
| Trans | Copilot.Theorem.Kind2 |
| Type | Copilot.Theorem.Kind2 |
| Universal | Copilot.Theorem.Prove, Copilot.Theorem |
| Unknown | Copilot.Theorem.Prove |
| UProof | Copilot.Theorem.Prove |
| Valid | Copilot.Theorem.Prove |
| ValueLiteral | Copilot.Theorem.Kind2 |
| varFlags | Copilot.Theorem.Kind2 |
| varId | Copilot.Theorem.Kind2 |
| varType | Copilot.Theorem.Kind2 |
| yices | Copilot.Theorem.Prover.SMT |
| z3 | Copilot.Theorem.Prover.SMT |