Def1 (nholz)

Def1 Module

This module defines a command for defining type bijection constants for a given type constant definition.

Function or value	Description
`get_all_type_bijection_info ()` Full Usage: `get_all_type_bijection_info ()` Parameters: () : `unit` Returns: `(string * ((string * string) * (thm * thm))) list`	() : `unit` Returns: `(string * ((string * string) * (thm * thm))) list`
`get_all_type_bijections ()` Full Usage: `get_all_type_bijections ()` Parameters: () : `unit` Returns: `(string * (thm * thm)) list`	() : `unit` Returns: `(string * (thm * thm)) list`
`get_type_bijection_info x` Full Usage: `get_type_bijection_info x` Parameters: x : `string` Returns: `(string * string) * (thm * thm)`	x : `string` Returns: `(string * string) * (thm * thm)`
`get_type_bijections x` Full Usage: `get_type_bijections x` Parameters: x : `string` Returns: `thm * thm`	x : `string` Returns: `thm * thm`
`new_type_bijections x (tyfn1, tyfn2)` Full Usage: `new_type_bijections x (tyfn1, tyfn2)` Parameters: x : `string` tyfn1 : `string` tyfn2 : `string` Returns: `thm * thm`	x : `string` tyfn1 : `string` tyfn2 : `string` Returns: `thm * thm`
`the_type_bijections` Full Usage: `the_type_bijections` Returns: `dltree<string, ((string * string) * (thm * thm))> ref`	Returns: `dltree<string, ((string * string) * (thm * thm))> ref`