bd89fdcSmall change to doc comment syntax (allow spaces before | or ^)Edwin Brady14 years ago 1ccd94aSyntax for documentation comments and :doc REPL commandEdwin Brady14 years ago 8464bc4Add field for documentation comments in abstract syntaxEdwin Brady14 years ago 96f3b9eFix nested parameters blocksEdwin Brady14 years ago 6d7a6aaChange 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.Edwin Brady14 years ago af66f25Added 'mutual' blocks Effect is to elaborate all types in the block before elaborating definitionsEdwin Brady14 years ago 5692e48Added "codata" Constructors of coinductive types evaluate arguments lazily. Corecursive functions do not reduce at compile time.Edwin Brady14 years ago 7b2bf5eAdded "partial" keyword and "%default" directiveEdwin Brady14 years ago 517acc1Namespace parsing improvements (for qualified operator names) thanks to Dirk UllrichEdwin Brady14 years ago ffc7b69First baby steps towards a new RTS (and towards removing epic dependency)Edwin Brady14 years ago fee6b51Fix reverse elaboration of dependent pairsEdwin Brady15 years ago 126eb94Remove 'prefix' keywordEdwin Brady15 years ago dcb9ca0Change meaning of alternative syntax (| a , b , ... |) Now takes the first alternative to elaborate,rather than requiring exactly one to work. Old behaviour reserved for disambiguating namespaces.Edwin Brady15 years ago de6bb41Added 'total' keyword and positivity checkEdwin Brady15 years ago 3b36802Record syntax (but no magic yet...)Edwin Brady15 years ago 67c5734Added case and pattern matching let bindings Also pattern matching bind in do notation case notation currently has limitations: - only works on simple types (each pattern must have the same type, more specifically) - return type needs to be known at the point of elaborationEdwin Brady15 years ago 9265e7cAdded 'public', 'abstract' and 'private' modifiers 'public' means export everything (name and definition) 'abstract' means export just the name 'private' means export nothing for data types and classes, 'abstract' means export the type/class name but not the members.Edwin Brady15 years ago 60c4ef9Added 'impossible' keywordEdwin Brady15 years ago 9f65713Fix name parsing for nested namespacesEdwin Brady15 years ago fa5f1cdNamespacesEdwin Brady15 years ago b26716aCollect cumulativity constraints on universesEdwin Brady15 years ago dbc607cDecorating names for namespacesEdwin Brady15 years ago 1807c65No letters in operatorsEdwin Brady15 years ago bbaa193Better representation of namesEdwin Brady15 years ago 4931c20Added Integer (but an Epic bug prevents them compiling properly)Edwin Brady15 years ago 169d8c0Elaborating instance declarationsEdwin Brady15 years ago be3a53aType class instance resolution, and some Num overloadingEdwin Brady15 years ago 6cc3c32Fix small elaboration bugEdwin Brady15 years ago ebcb29bAdded proof script traces for pasting into programEdwin Brady15 years ago 95a558bAdded = and reflEdwin Brady15 years ago 39b934cSugar for dependent pairsEdwin Brady15 years ago bf368abFirst attempt at with ruleEdwin Brady15 years ago 834a5e0Fix bug in applying syntax rulesEdwin Brady15 years ago 2402885Generic syntax declarations (see prelude.idr for example)Edwin Brady15 years ago a805f47Added constants and some primitive operationsEdwin Brady15 years ago 82585e7Some ghc 6.12 compatibilityEdwin Brady15 years ago 64b7cfdParsing high level data declarationsEdwin Brady15 years ago 3b297bcParsing declarations, keeping track of fixitiesEdwin Brady15 years ago ff5f762Rename Core to TTEdwin Brady15 years ago 0ae24f1Shift core TT into a separate directory (for ease of reuse)Edwin Brady15 years ago