Open GoogleCodeExporter opened 9 years ago
See also DisplayLang.Name: DSPINE, DHEAD, DSCOPE. They could be renamed to
DSpineRN, etc., being uniform with InTm/InTmRN, etc.
Original comment by pedag...@gmail.com
on 15 Aug 2010 at 2:11
We also use all capitals for terms and types containing references (e.g. VAL,
INTM, TY), reference kinds (DEFN, HOLE) and telescopes (TEL). I think this is a
useful convention to follow, but would not go so far as changing INTM and
friends.
Original comment by adamgundry
on 16 Aug 2010 at 7:34
Original issue reported on code.google.com by
pedag...@gmail.com
on 15 Aug 2010 at 10:19