[MetaPRL Users] any(x) \in T and extracts in general.

[James Caldwell]

Hi Aleksey,

A few more questions ...  (I've cc'd this message to metaprl-users too.)

I don't see the "any" term declared in itt_void (where I sort of expect to
see it)   Is it declared somewhere else ?  or is it not used?

I'm thinking maybe it's not there.  Reading this bit of code I went to look
for a declaration of any and can't seem to find it.

define unfoldInd<https://vedauwoo.cs.uwyo.edu:60000/session/1/content/itt_core/itt_nat/unfoldInd/>
:
defiItt_nat!ind{'n<|!!|>; 'base<|!!|>; k, l. 'up<|!!|>['k; 'l]}
defiItt_(displayed as *Ind*(n) where *Ind*(*n*) = *n* = 0 ⇒ *Ind*(*n*) =
base (*n* > 0) ⇒ *Ind*(*n*) = up[*n*; *Ind*(*n* - 1)]) ←─→
defiItt_*Ind*(n) where *Ind*(*n*) = ((*n* < 0) ⇒ *Ind*(*n*) = ·) (*n* = 0 ⇒
*Ind*(*n*) = base) ((0 < *n*) ⇒ *Ind*(*n*) = up[*n*; *Ind*(*n* - 1)])

I sort of expect the the case for n<0 to say something like  ((n<0) ⇒ *Ind*(
*n*) = any(n)).

We haven't played with extracts yet ... and I guess i don't even really know
where to look for them ...  if any isn't there ... what would the extract be
for e.g. void_elimination?
The  user-guide  <http://metaprl.org/user-guide/default.html>  says
something about declaring extracts, but it looks like the extracts are not
declared for rules in the itt theory ... is that true?   Maybe the ITT
theory is not the right one to be using ... or maybe no one has done much
with extracts in MetaPRL yet.

Thanks again,
Jim
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.metaprl.org/pipermail/metaprl-users/attachments/20070612/3df7c812/attachment.html