------------------
-- Introduction --
------------------

Some simple tools for agda-mode to make programming in Agda even more enjoyable.

------------------
-- Installation --
------------------

Copy the agda2-mode-improvements.el files to your agda-mode directory.
Update the agda2-mode.el file with the version from this repo or 
1) add

(load "agda2-mode-improvements")

at the end your agda2-mode.el, just before the

;;;;;;;;;;;;;;;;;;;;;;

(provide 'agda2-mode)
;;; agda2-mode.el ends here

lines.

2) add keybindings for the new features:

    ;; [] solve with theorem db
    (agda2-solve-with-db "\C-c\C-v" (local) "Auto with theorems from the given db (or global if none given)")
    ;; show current dbs
    (agda2-show-current-dbs "\C-c\C-x\C-s" (local global) "Show contents of all databases at this point")
    ;; with expression generating
    (agda2-add-with-exp            "\C-c\C-w"     (local) "Reify to a with expression")
    (agda2-add-with-exp-make-case  "\C-c\C-x\C-w" (local) "Reify to a with expression and make case")
    ;; stub generation
    (agda2-generate-function-stub "\C-cg" (global) "Generate a function stub from type declaration.")
    ;; fix line
    (agda2-fix-line "\C-c\C-x\C-f" (global) "Try to fix a line with broken patterns by changing them to ...")

To locate the directory with the emacs-lisp files for agda-mode type
 agda-mode locate
in your terminal.

--------------
-- Features --
--------------

Features started so far:

1) A simple lemma database support (see LemmaDatabaseTutorial.lagda)
2) A few functions for creating a with expression by writing it inside a goal (see WithClausesTutorial.lagda)

Smaller features:

1) generating a function body stub based on type signature:

   Example:

   given

   plus : Nat -> Nat -> Nat  -- cursor on this line or on the one below
   
   press C-c g to get

   plus : Nat -> Nat -> Nat
   plus x x' = ?

   with the cursor placed in the new goal.

2) deleting a broken pattern declaration and inserting '... | '
   * this is useful when Agda has generated an invalid pattern after matching on a variable that binds the
   result of a pattern matching. Pressing C-c C-x C-f (f for "fix") will replace the function name and all patterns
   that weren't introduced by the last with-expression with an "... | ". This is often sufficent to make the file
   type-check successfully.

   Example:

   given
 
   equal? : Nat -> Nat -> Bool
   equal? n m with n \?= m
   equal? n m | yes p = true   -- line A
   equal? n m | no ~p = false  -- line B

   placing the cursor on line A and firing C-c C-x C-f and then doing the same for line B will yield

   equal? : Nat -> Nat -> Bool
   equal? n m with n \?= m
   ... | yes p = true  
   ... | no ~p = false