git.iko.soy/Idris-dev
on 9f65713 help sign in
history ofsrc/Idris/Parser.hs
all commits
fa5f1cdNamespacesEdwin Brady 94d888bParsing and elaboration of alternativesEdwin Brady 07f12f9Separate elaboration of declarations and termsEdwin Brady 01ceeadNamesEdwin Brady 03d7d5eAllow type labels on lambdasEdwin Brady dbc607cDecorating names for namespacesEdwin Brady bbaa193Better representation of namesEdwin Brady ae3ad10Apply fromInteger for negative numbersEdwin Brady 925648aAdd %include directiveEdwin Brady 374fc26Add let x = t tacticEdwin Brady 8d83d07Type declarations of the form (x,y,z : A) -> BEdwin Brady e89453fAllow type labels on sigma bindingsEdwin Brady 1c49219Added provisional definitionsEdwin Brady 4931c20Added Integer (but an Epic bug prevents them compiling properly)Edwin Brady e530718Add fromInteger to Nat class; allow type labels on letEdwin Brady f1c7fafAdded tactics construct, and tactic sequencing/choiceEdwin Brady 71c1a0eExtension parsing, now deferring checks name is uniqueEdwin Brady 4a1324cDistinguish term syntax and pattern syntaxEdwin Brady 31d974bMore flexibility with syntax definitionsEdwin Brady 2e02cf6Logging optionsEdwin Brady 5afe678Added log/exp (and lib/link directives)Edwin Brady ffc64e3Add mechanism for simplification and function optionsEdwin Brady 169d8c0Elaborating instance declarationsEdwin Brady f2459a5Added class constraintsEdwin Brady 13d08bdElaborating class declarationsEdwin Brady 33710abParsing class and instance (but no elaboration yet)Edwin Brady 5528447Not really mini any more...Edwin Brady 229a99cBetter elaboration order; also changed instance argument syntax slightlyEdwin Brady be3a53aType class instance resolution, and some Num overloadingEdwin Brady 22546bc:r and :e at the REPL.Edwin Brady 1b1a055Improved where; implicit arguments now expanded during elaborationEdwin Brady 188dda5Tinkering with tactics and deferred definitionsEdwin Brady 58bd7c4Added rewrite tacticEdwin Brady 10b88aeAdded refine, focus, undoEdwin Brady ebcb29bAdded proof script traces for pasting into programEdwin Brady 551548cBeginning theorem prover interfaceEdwin Brady 3bdfa26Added [static] annotations (which do nothing yet) and state to evaluatorEdwin Brady b85965eparser tinkeringEdwin Brady 1155e79Laziness annotationsEdwin Brady 95a558bAdded = and reflEdwin Brady 5fbca2aFix with so that clauses are checked for matches against top level defnEdwin Brady 39b934cSugar for dependent pairsEdwin Brady 5e92c70When collecting implicit args in wheres, ignore names bound in above scopeEdwin Brady bf368abFirst attempt at with ruleEdwin Brady cc4eb28let bindings; fixed bug with simple lambda appEdwin Brady 796fa25BannerEdwin Brady 5f7eed8Propagate line numbers through applications and variablesEdwin Brady ec87a69Some effort at reporting line numbers of errors (top level of decl only)Edwin Brady 180e979Added builtins.idr and fixed a bug or twoEdwin Brady 834a5e0Fix bug in applying syntax rulesEdwin Brady