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

[Adam Chlipala]

On 07/09/2017 05:58 PM, Peter Brottveit Bock wrote:
> 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?

Yes, that's what I meant.  The added benefit is that you really do have 
exactly the proof terms you were looking for; they just have these extra 
names tacked on them, but you can ignore those from a formal perspective!