Code

History

Commits on master to src/TTImp35+
  1. Fix lambda multiplicity checkEdwin Brady committed 6 years ago4947a99
  2. Don't fully normalise LHSEdwin Brady committed 6 years ago2a0e5a4
  3. Evaluate primitives (fromInteger etc)Edwin Brady committed 6 years ago819c9d7
  4. Some inlining changesEdwin Brady committed 6 years ago3d8d076
  5. Merge pull request #292 from ohad/fully-abstract-recordsEdwin Brady committed 6 years ago627d2c2
  6. Erase the World, with careEdwin Brady committed 6 years agoac277ce
  7. bugfix: actually include keyword "default" for default implict record type argumentsOhad Kammar committed 6 years ago5af82be
  8. Add support for default implicit arguments in record typesOhad Kammar committed 6 years ago3043ac0
  9. Merge branch 'master' of github.com:edwinb/Idris2 into fully-abstract-recordsOhad Kammar committed 6 years agof777531
  10. Add commits back to parser, simplify case-split for (auto)implict arguments in recordsOhad Kammar committed 6 years ago1fcac7a
  11. Ignoring the World is inadvisableEdwin Brady committed 6 years ago4098078
  12. Merge branch 'master' of github.com:edwinb/Idris2 into fully-abstract-recordsOhad Kammar committed 6 years ago73d2e7b
  13. Add support for record auto implicit parameters in parserOhad Kammar committed 6 years ago43634e3
  14. Bugfix: differentiate between implicit and explicit arguments in the return type of the constructorOhad Kammar committed 6 years agocef456f
  15. Add syntax for implicit arguments to recordsOhad Kammar committed 6 years agoe6be2af
  16. Refactor to allow supporting implicit and rit annotations on records (without adding syntax for them)Ohad Kammar committed 6 years ago95da5a8
  17. Merge branch 'master' of github.com:edwinb/Idris2 into fully-abstract-recordsOhad Kammar committed 6 years ago0254ff1
  18. Erasure correctnessEdwin Brady committed 6 years ago849a1da
  19. Allow flagging types as externally definedEdwin Brady committed 6 years ago69a7640
  20. Fix where under multiple casesEdwin Brady committed 6 years ago0daece1
  21. Local definitions need to be namespacedEdwin Brady committed 6 years ago6e02ffc
  22. Erase %World for the purpose of newtypesEdwin Brady committed 6 years ago211fc35
  23. newtype optimisationEdwin Brady committed 6 years ago471a472
  24. Complete specialised definitionsEdwin Brady committed 6 years ago1b859fa
  25. Rename TTImp parser combinator `ifaceParam` to `recordParam` to better match its functionOhad Kammar committed 6 years agoeac27b6
  26. In record elaboration, refactor helper function jname into a local functionOhad Kammar committed 6 years ago0fe4021
  27. During record elaboration, refactor the type of the record into the where clauseOhad Kammar committed 6 years ago95f8879
  28. Start on specialisationEdwin Brady committed 6 years agod801d0d
  29. Syntax for flagging arguments to specialiseEdwin Brady committed 6 years ago2a81bd9
  30. Better disambiguation of pairsEdwin Brady committed 6 years agob3dc643
  31. Depth error are ambiguity errors tooEdwin Brady committed 6 years agoaaf07d5
  32. Report an error if ambiguities go too deepEdwin Brady committed 6 years agob417413
  33. Better ambiguity resolutionEdwin Brady committed 6 years ago736699c
  34. Small improvement in ambiguity resolutionEdwin Brady committed 6 years agoee3011a
  35. Better ambiguity errorsEdwin Brady committed 6 years ago6546113

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