The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

Hello all

 

I would like to use Notation to define a letrec-like syntax where binding occurrences of variables don’t occur in a simple list such as “exists x y, P” or “fun x y => M” but rather something like “letrec f = M and g = N in Q” (here, f and g are binders that scope over M, N and Q). I can’t see how to do this in an n-ary way (i.e. using a recursive notation). I can build arity-specific notation e.g. for the arity-2 example just given,  but for general n it doesn’t seem possible. Has anyone got a trick that I’ve missed?

 

Cheers

Andrew.