git.iko.soy/Idris-dev
on master help sign in
history of4afe404..master
compare
0dd7396Set totality of primitive operatorsEdwin Brady 1b7d089Recheck totality after an interactive proofEdwin Brady 9864c25Add :total commandEdwin Brady 7142d7eTotality checker tweaksEdwin Brady 63afafaMore additions to natural numbers theory.Dominic Mulligan 34c0ebbMerge remote-tracking branch 'upstream/master'Dominic Mulligan b1e95cbFix coverage checkerEdwin Brady 8079a69More additions to the Nat file.Dominic Mulligan 7fb7decImproved termination check (gets ackermann now, but still no mutual recursive definitions)Edwin Brady 486b176Some re-ordering of the tutorialEdwin Brady 141694fFix typoEdwin Brady 0f60127Update tutorial pdfEdwin Brady e200d08Added DSL file to tutorial (oops)Edwin Brady bb3e629Remark on types in instance blocksEdwin Brady 978479b(Try again...) Fixed some case statement bugsEdwin Brady 6f96ffaAdded some libraries, fixed some case statement bugsEdwin Brady db08df4Small record fix for implicit argumentsEdwin Brady 1effd22Fix lib/MakefileEdwin Brady 68194ceFix export of record fieldsEdwin Brady 88de6d0Update tutorial pdfEdwin Brady c4866f4More on idiomsEdwin Brady 7e2765bIdiom brackets and dsl notation in tutorialEdwin Brady 392c225Check definitions structurally as well as by name in conversionEdwin Brady 21c3a30Give up type class resolution soonerEdwin Brady 71ac2bcAdd records to tutorialEdwin Brady d54f335Added record testEdwin Brady 02501efChanged record update syntax... ...since {} is too overloaded now record { field = val } rec Also put records in their own namespaceEdwin Brady 4cd20b3Record update syntax { field = val } is a function which updates the field. So { field = val } rec update the field in record 'rec'. (This is backwards from Haskell, firstly because the other way round would conflict with implicit argument syntax, and secondly because it means record updates can be partially applied)Edwin Brady 7826c0eRecord update functions set_field val record -- updates the field name 'field' to 'val' in 'record'Edwin Brady 3a4a26bBetter dealing with names in patternsEdwin Brady 3c42704Record projectionEdwin Brady 34331d9Document auto implicitsEdwin Brady b752e2dMade tutorial and examples consistent with latest libraryEdwin Brady cfc12baBetter name-chasing in CompilerEdwin Brady 66bcd8cFix library compilation errors and improve name resolution in patternsEdwin Brady 092e30bMerge pull request #6 from dpmulligan/masterEdwin Brady 98be75cAdded (experimentally) auto implicit argumentsEdwin Brady 6dcf4c3Build a call graph and only compile things which are usedEdwin Brady 71705d5fixed name of module, renaming from my private module name to the correct name for addition in preludeDominic Mulligan bed7b3eBig load of theory on lists, and the start of a sketch of a hierarchy for numeric types.Dominic Mulligan b66ec2bMerge branch 'master' of https://github.com/dpmulligan/Idris-devEdwin Brady 32ab3b1Merge pull request #5 from IreneKnapp/masterEdwin Brady fc6eb53Bug fixes; checking type names in data declsEdwin Brady de6bb41Added 'total' keyword and positivity checkEdwin Brady 8baaa42Error message tinkerEdwin Brady 17cbae5Flip was in both builtins.idr and prelude.idr; it is now removed from the latter.Irene Knapp 2e994b8Implement "any" for lists. Obviously this is just the tip of an iceberg.Irene Knapp 7c59234Eq and Ord instances for lists and tuples.Irene Knapp b21db50New .gitignore for Cabal's directory and .ibc files.Irene Knapp 3e3cbfbSmall change to list.idr file removing stray qualified names.Dominic Mulligan