Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
#######
#
# E-scripts on Agda.
#
# Note 1: use the eev command (defined in eev.el) and the
# ee alias (in my .zshrc) to execute parts of this file.
# Executing this file as a whole makes no sense.
#
# Note 2: be VERY careful and make sure you understand what
# you're doing.
#
# Note 3: If you use a shell other than zsh things like |&
# and the for loops may not work.
#
# Note 4: I always run as root.
#
# Note 5: some parts are too old and don't work anymore. Some
# never worked.
#
# Note 6: the definitions for the find-xxxfile commands are on my
# .emacs.
#
# Note 7: if you see a strange command check my .zshrc -- it may
# be defined there as a function or an alias.
#
# Note 8: the sections without dates are always older than the
# sections with dates.
#
# This file is at <http://angg.twu.net/e/agda.e>
#           or at <http://angg.twu.net/e/agda.e.html>.
#        See also <http://angg.twu.net/emacs.html>,
#                 <http://angg.twu.net/.emacs[.html]>,
#                 <http://angg.twu.net/.zshrc[.html]>,
#                 <http://angg.twu.net/escripts.html>,
#             and <http://angg.twu.net/>.
#
#######




# «.agda-tutorials»	(to "agda-tutorials")
# «.agda-mode»		(to "agda-mode")
# «.interactive»	(to "interactive")



# (find-es "coq" "agda")
# (find-es "haskell" "agda2")

# (find-zsh "availabledebs | sort | grep agda")
# (find-status   "agda-bin")
# (find-vldifile "agda-bin.list")
# (find-udfile   "agda-bin/")
# (find-status   "agda-mode")
# (find-vldifile "agda-mode.list")
# (find-udfile   "agda-mode/")
# (find-status   "agda-stdlib-doc")
# (find-vldifile "agda-stdlib-doc.list")
# (find-udfile   "agda-stdlib-doc/")
# (find-status   "agda-stdlib")
# (find-vldifile "agda-stdlib.list")
# (find-udfile   "agda-stdlib/")
# (find-status   "haskell-agda-doc")
# (find-vldifile "haskell-agda-doc.list")
# (find-udfile   "haskell-agda-doc/")
# (find-status   "libghc6-agda-dev")
# (find-vldifile "libghc6-agda-dev.list")
# (find-udfile   "libghc6-agda-dev/")
# (find-status   "libghc6-agda-doc")
# (find-vldifile "libghc6-agda-doc.list")
# (find-udfile   "libghc6-agda-doc/")

# (find-fline "/etc/emacs/site-start.d/60agda-stdlib.el")
# (find-fline "/usr/lib/agda-stdlib/")
# (find-fline "/usr/share/doc/libghc6-agda-doc/html/")
# (find-udfile "libghc6-agda-doc/README.gz")



#####
#
# Agda tutorials
# 2010dec17
#
#####

# «agda-tutorials»  (to ".agda-tutorials")
# (find-angg ".emacs.papers" "agda")
# http://wiki.portal.chalmers.se/agda/
# http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Documentation
# http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials

# http://www.cs.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf
# http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
# http://wiki.portal.chalmers.se/agda/uploads/Main.Othertutorials/AgdaOverview2009.pdf

# http://permalink.gmane.org/gmane.comp.lang.agda/1579
# http://www.cl.cam.ac.uk/teaching/0910/L20/
# http://www.cl.cam.ac.uk/teaching/0910/L20/clex1.pdf
# http://www.cl.cam.ac.uk/teaching/0910/L20/clex2a.pdf
# http://www.cl.cam.ac.uk/teaching/0910/L20/clex3.pdf
# http://www.cl.cam.ac.uk/teaching/0910/L20/clex4.pdf
# http://www.cl.cam.ac.uk/~ss368/




#####
#
# The Agda mode for Emacs
# 2010dec17
#
#####

# «agda-mode»  (to ".agda-mode")
# (find-status   "agda-mode")
# (find-vldifile "agda-mode.list")
# (find-udfile   "agda-mode/")
# (find-udfile "agda-mode/README.gz")
# (find-sitelispfile "agda/")
# (find-sitelispfile "agda/agda-input.el")
# (agda-input-show-translations "Agda")
# (find-efunction 'agda-input-show-translations)

# http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput




#####
#
# Interactive mode
# 2011nov26
#
#####

# «interactive»  (to ".interactive")
# https://lists.chalmers.se/pipermail/agda/2011/002639.html
# http://wiki.portal.chalmers.se/agda/agda.php?n=Main.FeatureRequests
# http://www.cl.cam.ac.uk/teaching/1011/L20/

(defun eepitch-agda () (interactive)
  (eepitch-comint "agda" "agda -I"))

* (eepitch-agda)
* (eepitch-kill)
* (eepitch-agda)
:?
:eval 2 + 3



# http://news.gmane.org/gmane.comp.lang.agda
# http://unit.aist.go.jp/cvs/Agda/main.pdf

To generate highlighted, hyperlinked web pages from source code, run
the following command in a shell:

  agda --html --html-dir=<output directory> <root module>

You can change the way in which the code is highlighted by providing
your own CSS file instead of the default one (use the --css option).

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments
https://wiki.cse.unsw.edu.au/cs3141/10s1/Agda%20%26%20Haskell%20Resources

# Agda is similar to epigram:
# (find-es "haskell" "epigram")

http://agda.posterous.com/use-agda-input-mode-in-code



https://lists.chalmers.se/pipermail/agda/2011/003420.html






#  Local Variables:
#  coding:               raw-text-unix
#  ee-delimiter-hash:    "\n#*\n"
#  ee-delimiter-percent: "\n%*\n"
#  ee-anchor-format:     "«%s»"
#  End: