Subject: Objects

Keywords: ::proof

Title: How proofs are stored in the libary.

--------------------------------------------------

STM : object
  - statment of lemma
  - list of proofs.

PRF : object
  - inf_tree

INF : object
  - refinement
      * goal : sequent # annotation list
      * tactic 
      * partial extract
      * references
      * subgoals 
 ⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t
              :t

⋅

Home