on 496cf41 help sign in
all commits
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