git.iko.soy/Idris-dev
on ddba413 help sign in
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 bbaa193Better representation of namesEdwin Brady 34f92f3Fix deferred names in type declarationsEdwin Brady f9a0008Added 'believe_me'Edwin Brady ae3ad10Apply fromInteger for negative numbersEdwin Brady 325b919:t for names as well as termsEdwin Brady e20f401No holes allowedEdwin Brady 93946fcinsertImpl shouldn't crash if given too many argumentsEdwin Brady 925648aAdd %include directiveEdwin Brady 663c464Added test directory and a single test...Edwin Brady 374fc26Add let x = t tacticEdwin Brady df49a2awith fixEdwin Brady be2d7faCtrl-D now quits replEdwin Brady 9a59cb5Add FalseElim as a primitiveEdwin Brady da5e25eeither.idrEdwin Brady 8d83d07Type declarations of the form (x,y,z : A) -> BEdwin Brady 1309a42Give pi bindings unique namesEdwin Brady 048e2a7namesIn should look for *all* namesEdwin Brady 04ac1a8/= for FinEdwin Brady 72c2e2aEquality on FinEdwin Brady 4afe404Fix refine on local namesEdwin Brady e89453fAllow type labels on sigma bindingsEdwin Brady 1c49219Added provisional definitionsEdwin Brady d496a9c:e now reloads the edited fileEdwin Brady e0e52f1simple_app should try both elaboration ordersEdwin Brady f31caf5unique_hole needs to check whole contextEdwin Brady