Changes between Version 8 and Version 9 of Commentary/Compiler/CoreSynType


Ignore:
Timestamp:
Sep 14, 2006 8:55:08 PM (8 years ago)
Author:
nr
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/CoreSynType

    v8 v9  
    4545 * {{{Lam}}} is used for both term and type abstraction (small and big lambdas). 
    4646 
    47  * {{{Type}}} appears only in type-argument positions (e.g. {{{App (Var f) (Type ty)}}}).  To emphasise this, the type synonym {{{Arg}}} is used as documentation when we expect that a {{{Type}}} constructor may show up. 
     47 * {{{Type}}} appears only in type-argument positions (e.g. {{{App (Var f) (Type ty)}}}).  To emphasise this, the type synonym {{{Arg}}} is used as documentation when we expect that a {{{Type}}} constructor may show up.  Anything not called {{{Arg}}} should not use a {{{Type}}} constructor. 
    4848 
    4949 * {{{Let}}} handles both recursive and non-recursive let-bindings; see the the two constructors for {{{Bind}}}.