1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
\DOC parse_pretype
\TYPE {parse_pretype : lexcode list -> pretype * lexcode list}
\SYNOPSIS
Parses a pretype.
\DESCRIBE
The call {parse_pretype t}, where {t} is a list of lexical tokens (as produced
by {lex}), parses the tokens and returns a pretype as well as the unparsed
tokens.
\FAILURE
Fails if there is a syntax error in the token list.
\USES
This is mostly an internal function; pretypes and preterms are used as an
intermediate representation for typechecking and overload resolution and are
not normally of concern to users.
\SEEALSO
lex, parse_preterm, parse_term, parse_type.
\ENDDOC
|
