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 | Copilot.Theorem.Prover.SMT |
def | Copilot.Theorem.Prover.SMT, Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
Default | Copilot.Theorem.Prover.SMT, Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
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 | Copilot.Theorem.Prover.SMT |
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 | Copilot.Theorem.Prover.SMT |
mathsat | Copilot.Theorem.Prover.SMT |
maxK | Copilot.Theorem.Prover.SMT |
metit | Copilot.Theorem.Prover.SMT |
Modular | Copilot.Theorem.Kind2 |
onlySat | Copilot.Theorem.Prover.SMT |
onlyValidity | Copilot.Theorem.Prover.SMT |
Options | |
1 (Type/Class) | Copilot.Theorem.Prover.SMT |
2 (Data Constructor) | Copilot.Theorem.Prover.SMT |
3 (Type/Class) | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
4 (Data Constructor) | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
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 | Copilot.Theorem.Prover.SMT |
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 |