../ Core/Small change to doc comment syntax (allow spaces before | or ^)14 years ago IRTS/Change comment rules Comments cannot begin '{-|' or '--|'. This is now reserved for documentation comments, which will be part of the syntax to support documentation at the REPL.14 years ago Idris/Display useful information on :doc (It's ugly though...)14 years ago Pkg/Change comment rules Comments cannot begin '{-|' or '--|'. This is now reserved for documentation comments, which will be part of the syntax to support documentation at the REPL.14 years ago RTS/Added binding form to syntax rules (and updated tutorial accordingly)14 years ago Util/Added simple library packaging system Now used for the prelude (see lib/base.ipkg)14 years ago Main.hsMinor tutorial updates14 years ago