on 175a735 help sign in
all commits
f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen fb3f7f0Use At to hold FCsDavid Raymond Christiansen aed179cTrack the providence of unification errorsDavid Raymond Christiansen 7437ebePrepared data structure of FC for spanning, and added the span of the last token parsed to IdrisAhmad Salim Al-Sibahi 5987a95Report errors loading files using semantic highlightingDavid Raymond Christiansen 0c8c90dStrictness annotationsEdwin Brady 40da42fSupport names and terms in error reflectionDavid Raymond Christiansen b0e43f0Initial partial version of REPL error reflectionDavid Raymond Christiansen 5000aebAdd a Cabal libraryBrian McKenna b1537b9Report errors directly, instead of parsing the string given to ihputStrLnHannes Mehnert 3c32b65Whitespace cleanup.George Leontiev 57c8657Added column name to sourceAhmad Salim Al-Sibahi 53b28e6Update compiler to use new error handlingDavid Christiansen ac33945Wrap Idris in an ErrorTDavid Christiansen 66ff954Make the type of ierror more generalDavid Christiansen e49ab72Reorder the monad transformers in the Idris monad to allow completionDavid Christiansen e7c9256Allow inference of Sets at REPLEdwin Brady 72d4d96Starting unused argument analysisEdwin Brady c30e6ceNo need to qualify unambiguous names on :pEdwin Brady 392c225Check definitions structurally as well as by name in conversionEdwin Brady 7f74f91Fix error handling again in replEdwin Brady 4ca34ffFix error recovery in replEdwin Brady 49e426aSwitch from readline to haskelineMathnerd314 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 Brady b645699Don't write .ibc on error; add new testEdwin Brady 22546bc:r and :e at the REPL.Edwin Brady 551548cBeginning theorem prover interfaceEdwin Brady ec87a69Some effort at reporting line numbers of errors (top level of decl only)Edwin Brady 070b0faSome unification/evaluation bug fixesEdwin Brady f9fb363Tinkering with error reportingEdwin Brady 739e0b5Some error handlingEdwin Brady