[MetaPRL Users] some metaprl questions

[James Caldwell]

Hi Aleksey,

So ... we've been doing some stuff with the system but I'm missing some
tactics I want --- and I certainly don't understand how to do many things.

1.) I can seem to find Fold or FoldC .... there is something about folding
but I need to provide a conversion to do so?  Not sure how to do this, in
Nuprl I can just name the definition I'd like to fold (e.g. FoldC `foo`)

2.) I'm having some trouble with squiggle -- which I never really used in
Nuprl.  Do I understand correctly that t1 ~ t2 holds if I can rewrite t1 and
t2 into a common form?  If so, this would seem to mean that (for functions
anyway) this is a finer equality e.g.  there may be extensionally equal
functions which can never be reduced to alpha equivalent forms.
Is this right?  Comments?  Squiggle seems to play a larger role in metaprl's
itt theory than it does in vanilla Nuprl.  For example, you seem to support
(via rewriteC) a conversional for rewriting with squiggle, but don't have a
similar one for real equality.   Probably I'm just missing it.

3.)  In the meta-part of metaprl -- we can write something like C[x]  where
C is a context ... but surely there is nothing I can ever do to show
functionality for the slot in C.  This would seem to mean that we can't use
hypSubstT.  Is this right?  I guess we'd be OK with squiggle here though
because of the computation rule.


Jim
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.metaprl.org/pipermail/metaprl-users/attachments/20070621/6d972671/attachment.html