non_type_definitions

EmitTeX.non_type_definitions : string -> (string * thm) list

A versions of definitions that attempts to filter out definitions created by Hol_datatype.

An invocation non_type_definitions thy, where thy is the name of a currently loaded theory segment, will return a list of the definitions stored in that theory. Each definition is paired with its name in the result.

Failure

Never fails. If thy is not the name of a currently loaded theory segment, the empty list is returned.

Example

> new_theory "example";
<<HOL message: Restarting theory "example">>
<<HOL warning: Theory.callhooks: Hook Parse.clear_consts_from_grammar failed on event NewTheory{oldseg = "example", newseg = "example"} with problem 
Exception raised at Term.dest_thy_const: not a const
>>
val it = (): unit
> val _ = Hol_datatype `example = First | Second`;
<<HOL message: Defined type: "example">>
> val example_def = Define
   `(example First = Second) /\ (example Second = First)`;
Definition has been stored under "example_def"
val example_def = ⊢ example First = Second ∧ example Second = First: thm

> definitions "example";
val it =
   [("example_TY_DEF", ⊢ ∃rep. TYPE_DEFINITION (λn. n < 2) rep),
    ("example_size_def", ⊢ ∀x. example_size x = 0),
    ("example_def", ⊢ example First = Second ∧ example Second = First),
    ("example_CASE",
     ⊢ ∀x v0 v1.
         (case x of First => v0 | Second => v1) =
         (λm. if m = 0 then v0 else v1) (example2num x)),
    ("example_BIJ",
     ⊢ (∀a. num2example (example2num a) = a) ∧
       ∀r. (λn. n < 2) r ⇔ example2num (num2example r) = r)]:
   (string * thm) list

> EmitTeX.non_type_definitions "example";
val it =
   [("example_def", ⊢ example First = Second ∧ example Second = First)]:
   (string * thm) list

See also

DB.definitions, bossLib.Hol_datatype