Re: Question about notation

• To: types@UK.AC.GLA.DCS
• Subject: Re: Question about notation
• From: Libor Skarvada <libor@CS.MUNI.DCS.ADELARD>
• Date: Fri, 6 Nov 92 16:17:12 CET
• Approved: types@dcs.gla.ac.uk

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

• Prev: Question about notation
• Next: Notation query
• Index(es):
  • Main
  • Thread