git.iko.soy/Idris-dev
on cb47ec1 help sign in
history ofsrc/Core/CoreParser.hs
all commits
de6bb41Added 'total' keyword and positivity checkEdwin Brady 3b36802Record syntax (but no magic yet...)Edwin Brady 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 Brady 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 Brady 60c4ef9Added 'impossible' keywordEdwin Brady 9f65713Fix name parsing for nested namespacesEdwin Brady fa5f1cdNamespacesEdwin Brady b26716aCollect cumulativity constraints on universesEdwin Brady dbc607cDecorating names for namespacesEdwin Brady 1807c65No letters in operatorsEdwin Brady bbaa193Better representation of namesEdwin Brady 4931c20Added Integer (but an Epic bug prevents them compiling properly)Edwin Brady 169d8c0Elaborating instance declarationsEdwin Brady be3a53aType class instance resolution, and some Num overloadingEdwin Brady 6cc3c32Fix small elaboration bugEdwin Brady ebcb29bAdded proof script traces for pasting into programEdwin Brady 95a558bAdded = and reflEdwin Brady 39b934cSugar for dependent pairsEdwin Brady bf368abFirst attempt at with ruleEdwin Brady 834a5e0Fix bug in applying syntax rulesEdwin Brady 2402885Generic syntax declarations (see prelude.idr for example)Edwin Brady a805f47Added constants and some primitive operationsEdwin Brady 82585e7Some ghc 6.12 compatibilityEdwin Brady 64b7cfdParsing high level data declarationsEdwin Brady 3b297bcParsing declarations, keeping track of fixitiesEdwin Brady ff5f762Rename Core to TTEdwin Brady 0ae24f1Shift core TT into a separate directory (for ease of reuse)Edwin Brady