git.iko.soy/Idris-dev
on e2d0099 help sign in
e2d0099File handling in preludeEdwin Brady e06c1c1Makefile fix (thanks to Dirk Ullrich)Edwin Brady ec7c1b8Get cabal to check library after installEdwin Brady 6d01c6bCompile io bind specially, to make sure effectful thunks are not memoisedEdwin Brady 11d4feeSome file handlingEdwin Brady e261167Add some string primitives (may need latest Epic)Edwin Brady 72c7dbaSome more tutorialEdwin Brady 87946abShow user chosen names rather than machine onesEdwin Brady e5bc6f2A bit more tutorialEdwin Brady 8fbef42Started a new tutorial. Don't hold your breath.Edwin Brady dea8d48Added support for literate programming with bird tracks (use .lidr extension)Edwin Brady b645699Don't write .ibc on error; add new testEdwin Brady 215856dHmm, need to rethink the .cabal for installing .ibc filesEdwin Brady dccbc43Generate bytecode so that files don't need to be rechecked every time they're loadedEdwin Brady 8f77986Added some serialisationEdwin Brady 60c4ef9Added 'impossible' keywordEdwin Brady 7384683Fiddle with elaborator; update interp sample and testEdwin Brady 4ceba27Check pattern clauses have the same number of argumentsEdwin Brady 935f5e6Faster alternative resolutionEdwin Brady 3b5e50cAdded universe constraint checker and --typeintype command line optionEdwin Brady b2f6cc3A bit more preludeEdwin Brady f2e3a76Default definitions in classes, plus some bug fixingEdwin Brady be33671Don't search for type class instances we'll never solve - also allow default Int for NumEdwin Brady 9a2c916Update module namesEdwin Brady 40c303bSince we can overload things, might as well use less ugly names ;)Edwin Brady ddba413Fix buglet in Show instances for list/vectEdwin Brady c997a48Hierarchical namespaces; reorganised prelude accordinglyEdwin Brady 3b1ee4bMinor fix: don't add a proof more than onceEdwin Brady acb1f19Add :a comment, to add most recent proof script to source fileEdwin Brady 57c8ed3Added 'module' keyword to declare default namespace. 'main' must be in namespace 'main'Edwin Brady 6bef4f9Overloading lists and syntactic sugarEdwin Brady 598aca4Update interp example and test001 to use namespaces and overloading namesEdwin Brady 9f65713Fix name parsing for nested namespacesEdwin Brady fa5f1cdNamespacesEdwin Brady 536112dAdded Constraints.hs for universe constrain solving (but don't expect it to work yet...)Edwin Brady 8cd093fChanged lookup to return a list (preparation for namespaces)Edwin Brady 94d888bParsing and elaboration of alternativesEdwin Brady ada02deTinker with universe constraintsEdwin Brady 5b08cc9Add PAlternativeEdwin Brady 07f12f9Separate elaboration of declarations and termsEdwin Brady b26716aCollect cumulativity constraints on universesEdwin Brady 72b43b2Actually, better do that the other way around...Edwin Brady 895e66fType class resolution when there is inheritanceEdwin Brady 01ceeadNamesEdwin Brady 03d7d5eAllow type labels on lambdasEdwin Brady dbc607cDecorating names for namespacesEdwin Brady e473c2eExists namingEdwin Brady e713a98getWitness/getProofEdwin Brady bd793e2Better elaboration of Sigma (for better error messages)Edwin Brady 1807c65No letters in operatorsEdwin Brady