Code

History

Commits on master to src/TTImp/ProcessDef.idr35+
  1. Don't fully normalise LHSEdwin Brady committed 6 years ago2a0e5a4
  2. Fix where under multiple casesEdwin Brady committed 6 years ago0daece1
  3. Complete specialised definitionsEdwin Brady committed 6 years ago1b859fa
  4. Start on specialisationEdwin Brady committed 6 years agod801d0d
  5. Need to check multiplicity of names in LinearCheckEdwin Brady committed 6 years ago49510bf
  6. Don't build run time case trees for Rig0 defsEdwin Brady committed 6 years agoc1bc433
  7. Take environment into account in coverage checkEdwin Brady committed 6 years ago22febdf
  8. Coverage checker improvementEdwin Brady committed 6 years ago102fb7f
  9. Erase LHS before case tree compilationEdwin Brady committed 6 years agocd57190
  10. Add default implicit argumentsEdwin Brady committed 6 years ago2a2a208
  11. Coverage checker looks at 'impossible' clausesEdwin Brady committed 6 years ago57a14ff
  12. Record whether a definition originated from a holeEdwin Brady committed 6 years ago3bb5002
  13. Simpler implementation of 'case'Edwin Brady committed 6 years ago722131f
  14. Count argument position in parameter blocksEdwin Brady committed 6 years agoe5c7019
  15. Add %unbound_implicits directiveEdwin Brady committed 6 years agoc725d37
  16. Use a data type for dotting reasonEdwin Brady committed 6 years agoa26581f
  17. Better approach to erasure in pattern matchingEdwin Brady committed 6 years ago04e4ebf
  18. Add impossibility flag to ErasedEdwin Brady committed 6 years agofe74d6b
  19. Remove trailing whitespace from Idris sources.Michael Morgan committed 7 years agoe6121e0
  20. Don't write out metadata we don't needEdwin Brady committed 7 years ago131841b
  21. Allow deferring definitions to other modulesEdwin Brady committed 7 years ago9bb91b5
  22. Propagate implicits to with clausesEdwin Brady committed 7 years ago47ad8ee
  23. Fix possible loop in auto implicit searchEdwin Brady committed 7 years ago91262b4
  24. Don't pass let bound things to with functionEdwin Brady committed 7 years ago1119c08
  25. Make 'with' work in where blocksEdwin Brady committed 7 years ago11560a5
  26. Improve 'with' implementationEdwin Brady committed 7 years ago11199ac
  27. Initial attempt at RHS with applicationEdwin Brady committed 7 years agoccc5381
  28. Change equality elaborationEdwin Brady committed 7 years ago7c34fa1
  29. Substitute in 'simple' metavariable solutionsEdwin Brady committed 7 years ago2efaaa6
  30. More base librariesEdwin Brady committed 7 years ago0051488
  31. Need to save postponed names in ttc tooEdwin Brady committed 7 years agoeddb23d
  32. Updating typecase, add testsEdwin Brady committed 7 years agof9ea1ff
  33. Fix coverage checker issueEdwin Brady committed 7 years agocda87a9
  34. Add test for etaEdwin Brady committed 7 years ago9b44839
  35. Build and save references for metavars tooEdwin Brady committed 7 years agoce78aba

Keyboard shortcuts

General

Show keyboard shortcuts
?
Focus the current search
/

Issues and pull requests

Open filters
f

Issues, pull requests and Inbox

Select next item
j↓
Select previous item
k↑
Open selected item
Enter
Dismiss filters or clear selection
Esc

Repository code

Go to file
t