Hales estimates that almost 50% of his time formalising the Jordan curve theorem and working on Flyspeck was spent looking up theorems in the HOL Light library.
let rec loop (st : state) =
let cmd = read () in
let st', res = exec cmd st in
print res; loop st'
let rec loop (sts : state list) =
let cmd = read () in
let sts', res = exec cmd sts in
print res; loop sts'
type st = Stateid.t
val parse_sentence : st -> parsable -> vernac_expr
val add : ontop:st -> ?newtip:st -> vernac_expr -> st
val edit_at : Stateid.t -> `NewTip | `Focus of focus
val observe : Stateid.t -> unit
jsCoq, a thin layer over the STM
type state = {
system : States.state; (* summary + libstack *)
proof : Proof_global.state; (* proof state *) }
type transaction = type vernac_type =
| Cmd of cmd_t | VtStartProof of vernac_start
| Fork of fork_t | VtSideff of vernac_sideff_type
| Qed of qed_t | VtQed of vernac_qed_type
| Sideff of seff_t | VtProofStep of proof_step
| Alias of alias_t | VtProofMode of string
type vernac_when = | VtQuery of report_with
| VtNow | VtUnknown
| VtLater
val process_transaction : ast -> vernac_type * when -> unit
val reach : Stateid.t -> unit