Type (nholz)

Type Module

Namespace: HOL
Assembly: nholz.dll

This module defines the internal representation of HOL types. This is done by defining an abstract datatype for types, and then primitive syntax functions for constructing and destructing types, and support for type constant declaration. The primitive syntax constructors ensure that only well-formed types can be constructed. This module is a trusted component

Types

Type	Description
hol_type	This is the datatype for internal HOL types. It has 2 classes, corresponding to the 2 primitive syntactic categories of types: Type Variable denotes an occurrence of a type variable. It has just a name attribute. Any two occurrences of type variables within a given object represent the same entity iff they have the same name. Compound Type denotes an instance of a type constant. It has name and type parameter list attributes, where the name must be the name of a declared type constant, and the parameter list length must equal the declared type constant's arity.

Type

Description

hol_type

This is the datatype for internal HOL types. It has 2 classes, corresponding to the 2 primitive syntactic categories of types:

Type Variable denotes an occurrence of a type variable. It has just a name attribute. Any two occurrences of type variables within a given object represent the same entity iff they have the same name.

Compound Type denotes an instance of a type constant. It has name and type parameter list attributes, where the name must be the name of a declared type constant, and the parameter list length must equal the declared type constant's arity.

Functions and values

Function or value	Description
`dest_comp_type ty` Full Usage: `dest_comp_type ty` Parameters: ty : `hol_type` Returns: `string * hol_type list`	ty : `hol_type` Returns: `string * hol_type list`
`dest_fun_type ty` Full Usage: `dest_fun_type ty` Parameters: ty : `hol_type` Returns: `hol_type * hol_type`	Returns domain and range of a given function type ty : `hol_type` Returns: `hol_type * hol_type`
`dest_var_type ty` Full Usage: `dest_var_type ty` Parameters: ty : `hol_type` Returns: `string`	ty : `hol_type` Returns: `string`
`is_comp_type ty` Full Usage: `is_comp_type ty` Parameters: ty : `hol_type` Returns: `bool`	ty : `hol_type` Returns: `bool`
`is_fun_type ty` Full Usage: `is_fun_type ty` Parameters: ty : `hol_type` Returns: `bool`	Checks if a given type is a function type ty : `hol_type` Returns: `bool`
`is_tyconst_name x` Full Usage: `is_tyconst_name x` Parameters: x : `string` Returns: `bool`	The test for whether a given name is the name of a declared type constant. x : `string` Returns: `bool`
`is_var_type ty` Full Usage: `is_var_type ty` Parameters: ty : `hol_type` Returns: `bool`	ty : `hol_type` Returns: `bool`
`mk_comp_type (x, tys)` Full Usage: `mk_comp_type (x, tys)` Parameters: x : `string` tys : `hol_type list` Returns: `hol_type`	x : `string` tys : `hol_type list` Returns: `hol_type`
`mk_fun_type (ty1, ty2)` Full Usage: `mk_fun_type (ty1, ty2)` Parameters: ty1 : `hol_type` ty2 : `hol_type` Returns: `hol_type`	Creates a function type given a domain and range ty1 : `hol_type` ty2 : `hol_type` Returns: `hol_type`
`mk_var_type x` Full Usage: `mk_var_type x` Parameters: x : `string` Returns: `hol_type`	x : `string` Returns: `hol_type`
`prim_get_all_tyconsts ()` Full Usage: `prim_get_all_tyconsts ()` Parameters: () : `unit` Returns: `(string * BigInteger) list`	Returns the name and arity of each declared type constant. Arities are given as arbitrary precision integers. () : `unit` Returns: `(string * BigInteger) list`
`prim_get_tyconst_arity x` Full Usage: `prim_get_tyconst_arity x` Parameters: x : `string` Returns: `BigInteger`	Returns the arity of the type constant with the supplied name as an arbitrary precision integer. x : `string` Returns: `BigInteger`
`prim_new_tyconst (x, n)` Full Usage: `prim_new_tyconst (x, n)` Parameters: x : `string` n : `BigInteger`	This is the primitive declaration command for type constants. It takes a string and an arbitrary precision integer. The string becomes the name of a new type constant in the theory, and the integer becomes its arity. Any name can be used for a type constant, but supplying an existing type constant's name will cause failure. A note of the declaration is reported, and unit is returned. x : `string` n : `BigInteger`
`the_tyconsts` Full Usage: `the_tyconsts` Returns: `dltree<string, BigInteger> ref`	Returns: `dltree<string, BigInteger> ref`
`type_eq x y` Full Usage: `type_eq x y` Parameters: x : `hol_type` y : `hol_type` Returns: `bool`	Checks that the two terms are of the same type x : `hol_type` y : `hol_type` Returns: `bool`
`type_inst tytheta ty` Full Usage: `type_inst tytheta ty` Parameters: tytheta : `(hol_type * hol_type) list` ty : `hol_type` Returns: `hol_type`	tytheta : `(hol_type * hol_type) list` ty : `hol_type` Returns: `hol_type`
`type_inst0 tytheta ty` Full Usage: `type_inst0 tytheta ty` Parameters: tytheta : `(hol_type * hol_type) list` ty : `hol_type` Returns: `hol_type`	tytheta : `(hol_type * hol_type) list` ty : `hol_type` Returns: `hol_type`
`type_lt x y` Full Usage: `type_lt x y` Parameters: x : `hol_type` y : `hol_type` Returns: `bool`	x : `hol_type` y : `hol_type` Returns: `bool`