User Tools
pvs:prover
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
pvs:prover [2016/08/23 21:07] jonathan [Basic] |
pvs:prover [2017/09/14 16:08] (current) jonathan [Basic] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Interaction with Prover ====== | ====== Interaction with Prover ====== | ||
| + | |||
| ===== Basic ===== | ===== Basic ===== | ||
| Line 12: | Line 13: | ||
| * Prove the whole file: C-c C-p f | * Prove the whole file: C-c C-p f | ||
| * View prelude file: M-x vpf | * View prelude file: M-x vpf | ||
| + | * View proof status: ''M-x spf'' | ||
| + | * Display the proof in progress: ''M-x show-current-proof '' | ||
| ProofLite scripts can be created from proofs in two ways: | ProofLite scripts can be created from proofs in two ways: | ||
| Line 21: | Line 24: | ||
| formula is displayed in the bu ffer "ProofLite". | formula is displayed in the bu ffer "ProofLite". | ||
| + | ===== Commands ===== | ||
| + | * Introduce all types in formula: ''(all-typepreds)'' | ||
| + | * ''(typepred a b c)'' | ||
pvs/prover.1471986448.txt.gz · Last modified: 2016/08/23 21:07 by jonathan
Page Tools
