[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