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

Show
Ignore:
Timestamp:
09/14/06 13:55:08 (7 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}}}.