Def2 (nholz)

Def2 Module

Namespace: HOL
Assembly: nholz.dll

This module defines two specialised forms of definition for function constants. The first form is for non-recursive functions and the second is for recursive functions.

Functions and values

Function or value	Description
`bag_subtract xs ys` Full Usage: `bag_subtract xs ys` Parameters: xs : `'a list` ys : `'a list` Returns: `'a list`	xs : `'a list` ys : `'a list` Returns: `'a list`
`create_primrec_instns (f, conjinfoA) (arg3, conjinfoB)` Full Usage: `create_primrec_instns (f, conjinfoA) (arg3, conjinfoB)` Parameters: f : `term` conjinfoA : `('a * ('b list * term * (bool * int) list)) list` arg2 : `term * int` conjinfoB : `('a * (term list * term list * 'c * (int * term list) list * term)) list` Returns: `(hol_type * hol_type) list * (term * term) * (term * term) list * ('a * ('b * term) list) list`	f : `term` conjinfoA : `('a * ('b list * term * (bool * int) list)) list` arg2 : `term * int` conjinfoB : `('a * (term list * term list * 'c * (int * term list) list * term)) list` Returns: `(hol_type * hol_type) list * (term * term) * (term * term) list * ('a * ('b * term) list) list`
`def_term_info tm` Full Usage: `def_term_info tm` Parameters: tm : `term` Returns: `(term * int) * (term * (term list * term list * term list * (int * term list) list * term)) list`	tm : `term` Returns: `(term * int) * (term * (term list * term list * term list * (int * term list) list * term)) list`
`depair_instns u` Full Usage: `depair_instns u` Parameters: u : `term` Returns: `term * (term * term) list`	u : `term` Returns: `term * (term * term) list`
`depair_instns0 (tm, ty) u` Full Usage: `depair_instns0 (tm, ty) u` Parameters: tm : `term` ty : `hol_type` u : `term` Returns: `(term * term) list`	tm : `term` ty : `hol_type` u : `term` Returns: `(term * term) list`
`extract n xs` Full Usage: `extract n xs` Parameters: n : `int` xs : `'a list` Returns: `'a * 'a list`	n : `int` xs : `'a list` Returns: `'a * 'a list`
`flat_conjuncts_rule th` Full Usage: `flat_conjuncts_rule th` Parameters: th : `thm` Returns: `thm list`	th : `thm` Returns: `thm list`
`flat_conjuncts_rule0 ths th` Full Usage: `flat_conjuncts_rule0 ths th` Parameters: ths : `thm list` th : `thm` Returns: `thm list`	ths : `thm list` th : `thm` Returns: `thm list`
`fst_snd_conv tm` Full Usage: `fst_snd_conv tm` Parameters: tm : `term` Returns: `thm`	tm : `term` Returns: `thm`
`get_all_fun_definitions ()` Full Usage: `get_all_fun_definitions ()` Parameters: () : `unit` Returns: `(string * thm) list`	() : `unit` Returns: `(string * thm) list`
`get_fun_definition x` Full Usage: `get_fun_definition x` Parameters: x : `string` Returns: `thm`	x : `string` Returns: `thm`
`inject n x xs` Full Usage: `inject n x xs` Parameters: n : `int` x : `'a` xs : `'a list` Returns: `'a list`	n : `int` x : `'a` xs : `'a list` Returns: `'a list`
`new_fun_definition tm` Full Usage: `new_fun_definition tm` Parameters: tm : `term` Returns: `thm`	tm : `term` Returns: `thm`
`new_recursive_fun_definition th tm` Full Usage: `new_recursive_fun_definition th tm` Parameters: th : `thm` tm : `term` Returns: `thm`	th : `thm` tm : `term` Returns: `thm`
`primrec_theorem_info th` Full Usage: `primrec_theorem_info th` Parameters: th : `thm` Returns: `term * (term * (term list * term * (bool * int) list)) list`	th : `thm` Returns: `term * (term * (term list * term * (bool * int) list)) list`
`remove xs y` Full Usage: `remove xs y` Parameters: xs : `'a list` y : `'a` Returns: `'a list`	xs : `'a list` y : `'a` Returns: `'a list`
`strip_vararg_comb tm` Full Usage: `strip_vararg_comb tm` Parameters: tm : `term` Returns: `term * term list`	tm : `term` Returns: `term * term list`
`the_fun_defs` Full Usage: `the_fun_defs` Returns: `dltree<string, thm> ref`	Returns: `dltree<string, thm> ref`