extend_rectype_net : string * ('a * 'b * thm) -> unit

SYNOPSIS
Extends internal store of distinctness and injectivity theorems for a new inductive type.

DESCRIPTION
HOL Light maintains several data structures based on the current set of distinctness and injectivity theorems for the inductive data type so far defined. A call extend_rectype_net ("tyname",(_,_,rth)) where rth is the recursion theorem for the type as returned as the second item from define_type, extend these structures for a new type. Two arguments are ignored just for regularity with some other internal data structures.

FAILURE CONDITIONS
Never fails, even if the theorem is malformed.

COMMENTS
This function is called automatically by define_type, and normally users will not need to invoke it explicitly.

SEE ALSO
basic_rectype_net, define_type, distinctness_store, injectivity_store.