1\DOC gen_tyvar
2
3\TYPE {gen_tyvar : unit -> hol_type}
4
5\SYNOPSIS
6Generate a fresh type variable.
7
8\KEYWORDS
9variable, type.
10
11\LIBRARY
12Type
13
14\DESCRIBE
15An invocation {gen_tyvar()} generates a type variable {tyv} not
16seen in the current session. Furthermore, the concrete syntax
17of {tyv} is such that {tyv} is not obtainable by {mk_vartype},
18or by parsing.
19
20\FAILURE
21Never fails.
22
23\EXAMPLE
24{
25- gen_tyvar();
26> val it = `:%%gen_tyvar%%1` : hol_type
27
28- try Type `:%%gen_tyvar%%1`;
29
30Exception raised at Parse.hol_type parser:
31Couldn't make any sense with remaining input of "%%gen_tyvar%%1"
32
33- try mk_vartype "%%gen_tyvar%%1";
34
35Exception raised at Type.mk_vartype:
36incorrect syntax
37}
38
39
40\COMMENTS
41In general, the actual name returned by {gen_tyvar} should not be
42relied on.
43
44\USES
45Useful for coding some proof procedures.
46
47\SEEALSO
48Term.genvar, Term.variant.
49\ENDDOC
50