git.iko.soy/Idris-dev
on 536112d help sign in
history ofsrc/Core/CoreParser.hs
all commits
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