More forall-like operators

[Blaisorblade]

I've discovered that forall.fmt is in fact "extensible", and used it to define a bunch of other delimiters, though it's all a bit hacky.

% For correct parsing use as |exists (x: sigma). tau|.
% Parens are dropped, double them if you want them output.
%format exists(x) = exists_ x "\hsforall "
%format exists_ = "\exists "

and more ones. That includes even lambdas, after I've settled on the "sin" of writing lambda calculus using Haskell lambdas (so that when you see → in my thesis it can be a syntactic function space, a semantic one, a syntactic function or a semantic one—isn't that wonderful? My fault of course).

%format Pi = "\Pi"
%format PPi(x) = PPi_ x "\hsforall "
%format PPi_ = "\Pi "

%format Lambda = "\Lambda"
%format PLambda(x) = PLambda_ x "\hsforall "
%format PLambda_ = "\Lambda "

%format lambda = "\lambda"
%format plambda(x) = plambda_ x "\hsforall "
%format plambda_ = "\lambda "

% Untested:
%format mu = "\mu"
%format mmu x = mu x "\hsforall "