[TYPES] A doubt in AUTOMATH type system

Param Jyothi Reddy paramr at gmail.com
Sat Jan 7 00:50:13 EST 2006

I am trying to understand how automath lines could be interpreted in
PTS. in this regard i got stuck at the following. Any help would be

Can someone help me understand the meaning of p:PROP in the following Line:

in the paramters we have said that p:[x:Sigma]PROP. So how can p be
type fo PROP.

It is used as follows:

If i interpret paramters in definition of l_all as lambda then
l_all(sigma, p) reduces to p hence disallowing a1 : l_all(sigma, p).
Interpreting paramters as product is not possible because the body is
not correctly typed.


More information about the Types-list mailing list