basic_rectype_net : (int * (term -> thm)) net ref

- SYNOPSIS
- Net of injectivity and distinctness properties for recursive type constructors.
- DESCRIPTION
- HOL Light maintains a net of theorems used to simplify equations between elements of recursive datatypes; essentially these include injectivity and distinctness, e.g. CONS_11 and NOT_CONS_NIL for lists. This net is used in some situations where such things need to be proved automatically, notably in define. A call to basic_rectype_net() returns that net. It is automatically updated whenever a type is defined by define_type.
- FAILURE CONDITIONS
- Never fails.
- SEE ALSO
- cases, define, distinctness, GEN_BETA_CONV, injectivity.