[Ur] Generating fresh name (gensym :: {Unit} -> Name).

[Peter Brottveit Bock]

Thanks for the quick reply!

On Sun, 9 Jul 2017, at 23:22, Adam Chlipala wrote:
> Short answer: I can't think of any way to implement that feature, with 
> Ur as it stands today.
> 
> It seems consistent with the model of Ur in Coq, though the 
> representation of rows might need to be extended to allow iteration even 
> without a folder (to find a fresh name).

I honestly hadn't thought about the possibility of defining it within Ur, but
that's of course something I should have thought about. Anyway, to extend
Ur so that it is possible would require a non-trivial effort I guess.

> Well, you could combine the two: take in a polymorphic premise, but also 
> ask for a concrete disjoint name to be passed at the top level. The 
> implementation can instantiate the premise with the concrete name.

You mean something like

val lolli_right'' :
     n :: Name -> [[n] ~ gamma] =>
     t0 ::: Type -> t1 ::: Type -> gamma ::: {Type} ->
     (n :: Name -> [[n] ~ gamma] => lin (gamma ++ [n = t0]) t1) ->
     lin gamma (lolli t0 t1)

?

Yeah, that would be possible to implement, but it wouldn't really be an
improvement, would it? 

— Peter