Changes between Version 19 and Version 20 of Holes


Ignore:
Timestamp:
Apr 27, 2012 2:29:48 PM (3 years ago)
Author:
spl
Comment:

Remove now-unused section

Legend:

Unmodified
Added
Removed
Modified
  • Holes

    v19 v20  
    131131'''Stuff below here might be out of date; please edit'''
    132132
    133 = How we can almost do this in GHC now =
    134 GHC does not support holes in the way Agda does. It is possible to insert {{{undefined}}} in an expression to make it typecheck (which Agda doesn't have), but this is not very helpful when writing software. Inserting {{{undefined}}} only gives as information that the rest of the program typechecks, but will not help you find what you needed to use in its place. We propose to add an extension to GHC (and notably GHCi) to allow using holes, this page is meant to discuss the exact features and workflow of such an extension.
    135 
    136 First, two existing features that can be used as holes.
    137 
    138 
    139133= How this could be implemented in GHC =
    140134