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!
_______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
