a807a34Remove the unused arg from lookup functionsDavid Christiansen14 years ago 0970f01Disentangle Haskeline from the internals IdrisDavid Christiansen14 years ago e49ab72Reorder the monad transformers in the Idris monad to allow completionDavid Christiansen14 years ago dd5001fmake TT aware of Set -> Typeraichoo14 years ago 5602ea7A small cleanup after missing some stray ends in the diff.Dominic Mulligan15 years ago 8c64e9cGot pretty printing partially working using the Pretty type class as a replacement for Show. Now need to tweak it in order to make everything look nice, and to get terms printing correctly!Dominic Mulligan15 years ago 49e426aSwitch from readline to haskelineMathnerd31415 years ago 67c5734Added case and pattern matching let bindings Also pattern matching bind in do notation case notation currently has limitations: - only works on simple types (each pattern must have the same type, more specifically) - return type needs to be known at the point of elaborationEdwin Brady15 years ago 8cd093fChanged lookup to return a list (preparation for namespaces)Edwin Brady15 years ago 10b88aeAdded refine, focus, undoEdwin Brady15 years ago 06a81c9Elaborating types and data declarationsEdwin Brady15 years ago f85d1f0:ttshellEdwin Brady15 years ago aa85339Builds on ubuntu haskell platformEdwin Brady15 years ago ff5f762Rename Core to TTEdwin Brady15 years ago 0ae24f1Shift core TT into a separate directory (for ease of reuse)Edwin Brady15 years ago