[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)              %
%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%=%