dest_theory

DB.dest_theory : string -> theory

Return the contents of a theory.

An invocation dest_theory s returns a structure

   THEORY(s,{types, consts, parents, axioms, definitions, theorems})

where types is a list of (string,int) pairs that contains all the type operators declared in s, consts is a list of (string,hol_type) pairs enumerating all the term constants declared in s, parents is a list of strings denoting the parents of s, axioms is a list of (string,thm) pairs denoting the axioms asserted in s, definitions is a list of (string,thm) pairs denoting the definitions of s, and theorems is a list of (string,thm) pairs denoting the theorems proved and stored in s.

The call dest_theory "-" may be used to access the contents of the current theory.

Failure

If s is not the name of a loaded theory.

Example

> dest_theory "option";
val it =
   Theory: option
   
   Parents:
       one
       sum
   
   Type constants:
       option 1
   
   Term constants:
       IS_NONE              :α option -> bool
       IS_SOME              :α option -> bool
       NONE                 :α option
       OPTION_ALL           :(α -> bool) -> α option -> bool
       OPTION_APPLY         :(β -> α) option -> β option -> α option
       OPTION_BIND          :β option -> (β -> α option) -> α option
       OPTION_CHOICE        :α option -> α option -> α option
       OPTION_GUARD         :bool -> unit option
       OPTION_IGNORE_BIND   :β option -> α option -> α option
       OPTION_JOIN          :α option option -> α option
       OPTION_MAP           :(α -> β) -> α option -> β option
       OPTION_MAP2          :(β -> γ -> α) ->
       β option -> γ option -> α option
       OPTION_MCOMP         :(β -> α option) ->
       (γ -> β option) -> γ -> α option
       OPTREL               :(α -> β -> bool) -> α option -> β option -> bool
       SOME                 :α -> α option
       THE                  :α option -> α
       option_ABS           :α + unit -> α option
       option_CASE          :α option -> β -> (α -> β) -> β
       option_REP           :α option -> α + unit
       some                 :(α -> bool) -> α option
   
   Definitions:
       NONE_DEF
         ⊢ NONE = option_ABS (INR ())
       OPTION_ALL_def
         ⊢ (∀P. OPTION_ALL P NONE ⇔ T) ∧ ∀P x. OPTION_ALL P (SOME x) ⇔ P x
       OPTION_APPLY_def
         ⊢ (∀x. NONE <*> x = NONE) ∧ ∀f x. SOME f <*> x = OPTION_MAP f x
       OPTION_BIND_def
         ⊢ (∀f. OPTION_BIND NONE f = NONE) ∧
         ∀x f. OPTION_BIND (SOME x) f = f x
       OPTION_CHOICE_def
         ⊢ (∀m2. OPTION_CHOICE NONE m2 = m2) ∧
         ∀x m2. OPTION_CHOICE (SOME x) m2 = SOME x
       OPTION_GUARD_def
         ⊢ OPTION_GUARD T = SOME () ∧ OPTION_GUARD F = NONE
       OPTION_IGNORE_BIND_def
[...Output elided...]

Comments

A prettyprinter is installed for the type theory, but the contents may still be accessed via pattern matching.

See also

Hol_pp.print_theory