uptodate_type : hol_type -> bool
An invocation uptodate_type ty, checks ty to see if it has been built from any out of date components, returning false just in case it has. The definition of out-of-date is mutually recursive among types, terms, and theorems. A type variable never out-of-date. A compound type is out-of-date if either (a) its type operator is out-of-date, or (b) any of its argument types are out-of-date. A type operator is out-of-date if it has been re-declared or if the witness theorem used to justify the type in the call to new_type_definition is out-of-date. Only a component of the current theory segment may be out-of-date. All items from ancestor theories are fixed, and unable to be overwritten, thus are always up-to-date.
- Hol_datatype `foo = A | B of 'a`; <<HOL message: Defined type: "foo">> > val it = () : unit - val ty = Type `:'a foo list`; > val ty = `:'a foo list` : hol_type - uptodate_type ty; > val it = true : bool - delete_type "foo"; > val it = () : unit - uptodate_type ty; > val it = false : bool