[TYPES] A doubt in AUTOMATH type system
Param Jyothi Reddy
paramr at gmail.com
Sat Jan 7 00:50:13 EST 2006
Hi,
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
appreciated.
Can someone help me understand the meaning of p:PROP in the following Line:
@[sigma:TYPE][p:[x:sigma]PROP]
l_all:=p:PROP
in the paramters we have said that p:[x:Sigma]PROP. So how can p be
type fo PROP.
It is used as follows:
@[sigma:TYPE][p:[x:sigma]PROP][a1:l_all(sigma,p)][s:sigma]
l_alle:=<s>a1:<s>p
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.
Regards,
Param
More information about the Types-list
mailing list