[Prev][Next][Index][Thread]
Re: Question about notation
Andrew Pitts writes:
>
> \Gamma |- M has type tau
>
> should be called a "typing assertion", or to be more Swedish, a "typing
> judgement".
>
> Andy Pitts
>
I prefer
\Gamma \rhd M : \tau % \rhd is a small triangle pointing to the right
to
\Gamma \vdash M : \tau % \vdash is \TeX's name for |-
because `|-' is traditionally used for derivability of judgements, so
\vdash \Gamma \rhd M : \tau
means that judgement $\Gamma \rhd M:\tau$ is derivable according to
given rules.
--
%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%
% Libor Skarvada Department of Computer Science %
% Masaryk University, Brno, Czechoslovakia %
% libor@dcs.muni.cs phone: +42-5-757000 (x369) %
%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%