[Pkg-haskell-commits] [agda] 03/07: Merge tag 'upstream/2.4.0.2'
Iain Lane
laney at moszumanska.debian.org
Tue Aug 5 09:25:29 UTC 2014
This is an automated email from the git hooks/post-receive script.
laney pushed a commit to branch master
in repository agda.
commit fc46a08ab3f2136c5fc0595cc7c571d042b20229
Merge: 126a250 6e140ac
Author: Iain Lane <iain at orangesquash.org.uk>
Date: Tue Aug 5 03:38:58 2014 +0100
Merge tag 'upstream/2.4.0.2'
Upstream version 2.4.0.2
.authorspellings | 7 -
.cvsignore | 10 -
.darcsignore | 75 -
Agda.cabal | 130 +-
CHANGELOG | 4093 ++++++++++++
HACKING | 48 -
LICENSE | 11 +-
Makefile | 289 -
README | 6 +-
Setup.hs | 31 +-
TODO | 336 -
aclocal.m4 | 5 -
benchmark/Benchmark.hs | 199 -
benchmark/Makefile | 40 -
benchmark/Syntacticosmos/Basics.agda | 9 -
benchmark/Syntacticosmos/Cxt.agda | 41 -
benchmark/Syntacticosmos/Eta.agda | 51 -
benchmark/Syntacticosmos/Inst.agda | 61 -
benchmark/Syntacticosmos/Kind.agda | 12 -
benchmark/Syntacticosmos/Loc.agda | 63 -
benchmark/Syntacticosmos/Nom.agda | 89 -
benchmark/Syntacticosmos/Pr.agda | 92 -
benchmark/Syntacticosmos/README | 137 -
benchmark/Syntacticosmos/Shift.agda | 51 -
benchmark/Syntacticosmos/Subst.agda | 61 -
benchmark/Syntacticosmos/Syntacticosmos.agda | 22 -
benchmark/Syntacticosmos/Term.agda | 128 -
benchmark/Syntacticosmos/UntypedLambda.agda | 43 -
benchmark/ac/AC.agda | 193 -
benchmark/ac/Bool.agda | 67 -
benchmark/ac/EqProof.agda | 22 -
benchmark/ac/Example.agda | 49 -
benchmark/ac/Fin.agda | 63 -
benchmark/ac/List.agda | 44 -
benchmark/ac/Logic.agda | 8 -
benchmark/ac/Makefile | 20 -
benchmark/ac/Nat.agda | 36 -
benchmark/ac/Vec.agda | 42 -
benchmark/categories/Categories.agda | 66 -
benchmark/categories/Primitive.agda | 105 -
benchmark/cwf/Chain.agda | 24 -
benchmark/cwf/CwF.agda | 150 -
benchmark/cwf/Setoid.agda | 322 -
benchmark/emacs | 64 -
benchmark/logs/20071213-12.58-dhcp-246-168/ac1 | 35 -
benchmark/logs/20071213-12.58-dhcp-246-168/ac2 | 35 -
benchmark/logs/20071213-12.58-dhcp-246-168/ac3 | 35 -
benchmark/logs/20071213-12.58-dhcp-246-168/cat | 35 -
benchmark/logs/20071219-11.21-livia/ac1 | 50 -
benchmark/logs/20071219-11.21-livia/ac2 | 50 -
benchmark/logs/20071219-11.21-livia/ac3 | 50 -
benchmark/logs/20071219-11.21-livia/cat | 50 -
benchmark/logs/20080306-11.43-livia/ac1 | 50 -
benchmark/logs/20080306-11.43-livia/ac2 | 50 -
benchmark/logs/20080306-11.43-livia/ac3 | 50 -
benchmark/logs/20080306-11.43-livia/cat | 50 -
benchmark/logs/20080306-11.43-livia/syntax1 | 50 -
benchmark/logs/20080306-11.43-livia/syntax2 | 50 -
benchmark/logs/20080306-11.59-livia/README | 1 -
benchmark/logs/20080306-11.59-livia/ac1 | 50 -
benchmark/logs/20080306-11.59-livia/ac2 | 50 -
benchmark/logs/20080306-11.59-livia/ac3 | 50 -
benchmark/logs/20080306-11.59-livia/cat | 50 -
benchmark/logs/20080306-11.59-livia/syntax1 | 50 -
benchmark/logs/20080306-11.59-livia/syntax2 | 50 -
benchmark/logs/20080407-14.00-dhcp-243-41/ac1 | 34 -
benchmark/logs/20080407-14.00-dhcp-243-41/ac2 | 34 -
benchmark/logs/20080407-14.00-dhcp-243-41/ac3 | 34 -
benchmark/logs/20080407-14.00-dhcp-243-41/cat | 34 -
benchmark/logs/20080407-14.00-dhcp-243-41/cwf | 34 -
benchmark/logs/20080407-14.00-dhcp-243-41/syntax1 | 34 -
benchmark/logs/20080407-14.00-dhcp-243-41/syntax2 | 34 -
.../20080730-12.47-ulf-norells-macbook-pro/ac1 | 34 -
.../20080730-12.47-ulf-norells-macbook-pro/ac2 | 34 -
.../20080730-12.47-ulf-norells-macbook-pro/ac3 | 34 -
.../20080730-12.47-ulf-norells-macbook-pro/cat | 34 -
.../20080730-12.47-ulf-norells-macbook-pro/cwf | 34 -
.../20080730-12.47-ulf-norells-macbook-pro/syntax1 | 34 -
.../20080730-12.47-ulf-norells-macbook-pro/syntax2 | 34 -
.../20081126-12.59-ulf-norells-macbook-pro/README | 2 -
.../20081126-12.59-ulf-norells-macbook-pro/ac1 | 34 -
.../20081126-12.59-ulf-norells-macbook-pro/ac2 | 34 -
.../20081126-12.59-ulf-norells-macbook-pro/ac3 | 34 -
.../20081126-12.59-ulf-norells-macbook-pro/cat | 34 -
.../20081126-12.59-ulf-norells-macbook-pro/cwf | 34 -
.../20081126-12.59-ulf-norells-macbook-pro/syntax1 | 34 -
.../20081126-12.59-ulf-norells-macbook-pro/syntax2 | 34 -
.../20081126-15.26-ulf-norells-macbook-pro/README | 2 -
.../20081126-15.26-ulf-norells-macbook-pro/ac1 | 34 -
.../20081126-15.26-ulf-norells-macbook-pro/ac2 | 34 -
.../20081126-15.26-ulf-norells-macbook-pro/ac3 | 34 -
.../20081126-15.26-ulf-norells-macbook-pro/cat | 34 -
.../20081126-15.26-ulf-norells-macbook-pro/cwf | 34 -
.../20081126-15.26-ulf-norells-macbook-pro/syntax1 | 34 -
.../20081126-15.26-ulf-norells-macbook-pro/syntax2 | 34 -
.../20081127-09.18-ulf-norells-macbook-pro/ac1 | 34 -
.../20081127-09.18-ulf-norells-macbook-pro/ac2 | 34 -
.../20081127-09.18-ulf-norells-macbook-pro/ac3 | 34 -
.../20081127-09.18-ulf-norells-macbook-pro/cat | 34 -
.../20081127-09.18-ulf-norells-macbook-pro/cwf | 34 -
.../20081127-09.18-ulf-norells-macbook-pro/syntax1 | 34 -
.../20081127-09.18-ulf-norells-macbook-pro/syntax2 | 34 -
.../20081127-21.23-ulf-norells-macbook-pro/README | 1 -
.../20081127-21.23-ulf-norells-macbook-pro/ac1 | 34 -
.../20081127-21.23-ulf-norells-macbook-pro/ac2 | 34 -
.../20081127-21.23-ulf-norells-macbook-pro/ac3 | 34 -
.../20081127-21.23-ulf-norells-macbook-pro/cat | 34 -
.../20081127-21.23-ulf-norells-macbook-pro/cwf | 34 -
.../20081127-21.23-ulf-norells-macbook-pro/syntax1 | 34 -
.../20081127-21.23-ulf-norells-macbook-pro/syntax2 | 34 -
.../20081201-12.53-ulf-norells-macbook-pro/ac1 | 34 -
.../20081201-12.53-ulf-norells-macbook-pro/ac2 | 34 -
.../20081201-12.53-ulf-norells-macbook-pro/ac3 | 34 -
.../20081201-12.53-ulf-norells-macbook-pro/cat | 34 -
.../20081201-12.53-ulf-norells-macbook-pro/cwf | 34 -
.../20081201-12.53-ulf-norells-macbook-pro/syntax1 | 34 -
.../20081201-12.53-ulf-norells-macbook-pro/syntax2 | 34 -
.../20081201-12.55-ulf-norells-macbook-pro/README | 1 -
.../20081201-12.55-ulf-norells-macbook-pro/ac1 | 34 -
.../20081201-12.55-ulf-norells-macbook-pro/ac2 | 34 -
.../20081201-12.55-ulf-norells-macbook-pro/ac3 | 34 -
.../20081201-12.55-ulf-norells-macbook-pro/cat | 34 -
.../20081201-12.55-ulf-norells-macbook-pro/cwf | 34 -
.../20081201-12.55-ulf-norells-macbook-pro/syntax1 | 34 -
.../20081201-12.55-ulf-norells-macbook-pro/syntax2 | 34 -
.../20081201-13.09-ulf-norells-macbook-pro/ac1 | 34 -
.../20081201-13.09-ulf-norells-macbook-pro/ac2 | 34 -
.../20081201-13.09-ulf-norells-macbook-pro/ac3 | 34 -
.../20081201-13.09-ulf-norells-macbook-pro/cat | 34 -
.../20081201-13.09-ulf-norells-macbook-pro/cwf | 34 -
.../20081201-13.09-ulf-norells-macbook-pro/monad | 34 -
.../20081201-13.09-ulf-norells-macbook-pro/syntax1 | 34 -
.../20081201-13.09-ulf-norells-macbook-pro/syntax2 | 34 -
.../20090423-08.30-ulf-norells-macbook-pro/ac1 | 33 -
.../20090423-08.30-ulf-norells-macbook-pro/ac2 | 33 -
.../20090423-08.30-ulf-norells-macbook-pro/ac3 | 33 -
.../20090423-08.30-ulf-norells-macbook-pro/cat | 33 -
.../20090423-08.30-ulf-norells-macbook-pro/cwf | 33 -
.../20090423-08.30-ulf-norells-macbook-pro/monad | 33 -
.../20090423-08.30-ulf-norells-macbook-pro/syntax1 | 33 -
.../20090423-08.30-ulf-norells-macbook-pro/syntax2 | 33 -
benchmark/logs/20100113-19.32-dhcp-20-76/ac1 | 33 -
benchmark/logs/20100113-19.32-dhcp-20-76/ac2 | 33 -
benchmark/logs/20100113-19.32-dhcp-20-76/ac3 | 33 -
benchmark/logs/20100113-19.32-dhcp-20-76/cat | 33 -
benchmark/logs/20100113-19.32-dhcp-20-76/cwf | 33 -
benchmark/logs/20100113-19.32-dhcp-20-76/monad | 22 -
benchmark/logs/20100113-19.32-dhcp-20-76/syntax1 | 33 -
benchmark/logs/20100113-19.32-dhcp-20-76/syntax2 | 33 -
.../20110629-21.47-ulf-norells-macbook-pro/ac1 | 33 -
.../20110629-21.47-ulf-norells-macbook-pro/ac2 | 33 -
.../20110629-21.47-ulf-norells-macbook-pro/ac3 | 33 -
.../20110629-21.47-ulf-norells-macbook-pro/cat | 33 -
.../20110629-21.47-ulf-norells-macbook-pro/cwf | 33 -
.../20110629-21.47-ulf-norells-macbook-pro/functor | 33 -
.../latemeta | 33 -
.../20110629-21.47-ulf-norells-macbook-pro/monad | 33 -
.../polyfunctor | 33 -
.../20110629-21.47-ulf-norells-macbook-pro/syntax1 | 33 -
.../20110629-21.47-ulf-norells-macbook-pro/syntax2 | 33 -
benchmark/logs/20110701-09.48-dhcp-183029/ac1 | 33 -
benchmark/logs/20110701-09.48-dhcp-183029/ac2 | 33 -
benchmark/logs/20110701-09.48-dhcp-183029/ac3 | 33 -
benchmark/logs/20110701-09.48-dhcp-183029/cat | 33 -
benchmark/logs/20110701-09.48-dhcp-183029/cwf | 33 -
benchmark/logs/20110701-09.48-dhcp-183029/functor | 33 -
benchmark/logs/20110701-09.48-dhcp-183029/latemeta | 33 -
benchmark/logs/20110701-09.48-dhcp-183029/monad | 33 -
.../logs/20110701-09.48-dhcp-183029/polyfunctor | 33 -
benchmark/logs/20110701-09.48-dhcp-183029/syntax1 | 33 -
benchmark/logs/20110701-09.48-dhcp-183029/syntax2 | 33 -
benchmark/logs/20110706-10.42-dhcp-186038/ac1 | 51 -
benchmark/logs/20110706-10.42-dhcp-186038/ac2 | 53 -
benchmark/logs/20110706-10.42-dhcp-186038/ac3 | 33 -
benchmark/logs/20110706-10.42-dhcp-186038/cat | 35 -
benchmark/logs/20110706-10.42-dhcp-186038/cwf | 41 -
benchmark/logs/20110706-10.42-dhcp-186038/functor | 35 -
benchmark/logs/20110706-10.42-dhcp-186038/latemeta | 35 -
benchmark/logs/20110706-10.42-dhcp-186038/monad | 36 -
.../logs/20110706-10.42-dhcp-186038/polyfunctor | 36 -
benchmark/logs/20110706-10.42-dhcp-186038/syntax1 | 68 -
benchmark/logs/20110706-10.42-dhcp-186038/syntax2 | 33 -
benchmark/logs/20110706-16.14-dhcp-186038/ac1 | 51 -
benchmark/logs/20110706-16.14-dhcp-186038/ac2 | 53 -
benchmark/logs/20110706-16.14-dhcp-186038/ac3 | 33 -
benchmark/logs/20110706-16.14-dhcp-186038/cat | 35 -
benchmark/logs/20110706-16.14-dhcp-186038/cwf | 41 -
benchmark/logs/20110706-16.14-dhcp-186038/functor | 35 -
benchmark/logs/20110706-16.14-dhcp-186038/latemeta | 35 -
benchmark/logs/20110706-16.14-dhcp-186038/monad | 36 -
.../logs/20110706-16.14-dhcp-186038/monadpostulate | 36 -
.../logs/20110706-16.14-dhcp-186038/polyfunctor | 36 -
benchmark/logs/20110706-16.14-dhcp-186038/syntax1 | 68 -
benchmark/logs/20110706-16.14-dhcp-186038/syntax2 | 33 -
benchmark/logs/20110822-09.36-dhcp-190251/ac1 | 51 -
benchmark/logs/20110822-09.36-dhcp-190251/ac2 | 53 -
benchmark/logs/20110822-09.36-dhcp-190251/ac3 | 33 -
benchmark/logs/20110822-09.36-dhcp-190251/cat | 35 -
benchmark/logs/20110822-09.36-dhcp-190251/cwf | 41 -
benchmark/logs/20110822-09.36-dhcp-190251/functor | 35 -
benchmark/logs/20110822-09.36-dhcp-190251/latemeta | 35 -
benchmark/logs/20110822-09.36-dhcp-190251/monad | 36 -
.../logs/20110822-09.36-dhcp-190251/monadpostulate | 36 -
.../logs/20110822-09.36-dhcp-190251/polyfunctor | 36 -
benchmark/logs/20110822-09.36-dhcp-190251/prim | 35 -
benchmark/logs/20110822-09.36-dhcp-190251/syntax1 | 68 -
benchmark/logs/20110822-09.36-dhcp-190251/syntax2 | 33 -
benchmark/logs/20110822-13.57-dhcp-190251/ac1 | 51 -
benchmark/logs/20110822-13.57-dhcp-190251/ac2 | 53 -
benchmark/logs/20110822-13.57-dhcp-190251/ac3 | 33 -
benchmark/logs/20110822-13.57-dhcp-190251/cat | 35 -
benchmark/logs/20110822-13.57-dhcp-190251/cwf | 41 -
benchmark/logs/20110822-13.57-dhcp-190251/functor | 35 -
benchmark/logs/20110822-13.57-dhcp-190251/latemeta | 35 -
benchmark/logs/20110822-13.57-dhcp-190251/monad | 36 -
.../logs/20110822-13.57-dhcp-190251/monadpostulate | 36 -
.../logs/20110822-13.57-dhcp-190251/polyfunctor | 36 -
benchmark/logs/20110822-13.57-dhcp-190251/prim | 35 -
benchmark/logs/20110822-13.57-dhcp-190251/syntax1 | 68 -
benchmark/logs/20110822-13.57-dhcp-190251/syntax2 | 33 -
.../20110823-07.51-ulf-norells-macbook-pro/ac1 | 51 -
.../20110823-07.51-ulf-norells-macbook-pro/ac2 | 53 -
.../20110823-07.51-ulf-norells-macbook-pro/ac3 | 33 -
.../20110823-07.51-ulf-norells-macbook-pro/cat | 35 -
.../20110823-07.51-ulf-norells-macbook-pro/cwf | 41 -
.../20110823-07.51-ulf-norells-macbook-pro/functor | 35 -
.../latemeta | 35 -
.../20110823-07.51-ulf-norells-macbook-pro/monad | 36 -
.../monadpostulate | 36 -
.../polyfunctor | 36 -
.../20110823-07.51-ulf-norells-macbook-pro/prim | 35 -
.../20110823-07.51-ulf-norells-macbook-pro/syntax1 | 68 -
.../20110823-07.51-ulf-norells-macbook-pro/syntax2 | 33 -
.../20110823-08.00-ulf-norells-macbook-pro/ac1 | 51 -
.../20110823-08.00-ulf-norells-macbook-pro/ac2 | 53 -
.../20110823-08.00-ulf-norells-macbook-pro/ac3 | 33 -
.../20110823-08.00-ulf-norells-macbook-pro/cat | 35 -
.../20110823-08.00-ulf-norells-macbook-pro/cwf | 41 -
.../20110823-08.00-ulf-norells-macbook-pro/functor | 35 -
.../latemeta | 35 -
.../20110823-08.00-ulf-norells-macbook-pro/monad | 36 -
.../monadpostulate | 36 -
.../polyfunctor | 36 -
.../20110823-08.00-ulf-norells-macbook-pro/prim | 35 -
.../20110823-08.00-ulf-norells-macbook-pro/syntax1 | 68 -
.../20110823-08.00-ulf-norells-macbook-pro/syntax2 | 33 -
.../20110824-18.56-ulf-norells-macbook-pro/ac1 | 51 -
.../20110824-18.56-ulf-norells-macbook-pro/ac2 | 53 -
.../20110824-18.56-ulf-norells-macbook-pro/ac3 | 33 -
.../20110824-18.56-ulf-norells-macbook-pro/cat | 35 -
.../20110824-18.56-ulf-norells-macbook-pro/cwf | 41 -
.../20110824-18.56-ulf-norells-macbook-pro/functor | 35 -
.../latemeta | 35 -
.../20110824-18.56-ulf-norells-macbook-pro/monad | 36 -
.../monadpostulate | 36 -
.../polyfunctor | 36 -
.../20110824-18.56-ulf-norells-macbook-pro/prim | 35 -
.../20110824-18.56-ulf-norells-macbook-pro/syntax1 | 68 -
.../20110824-18.56-ulf-norells-macbook-pro/syntax2 | 33 -
.../20110825-14.57-ulf-norells-macbook-pro/ac1 | 51 -
.../20110825-14.57-ulf-norells-macbook-pro/ac2 | 53 -
.../20110825-14.57-ulf-norells-macbook-pro/ac3 | 33 -
.../20110825-14.57-ulf-norells-macbook-pro/cat | 35 -
.../20110825-14.57-ulf-norells-macbook-pro/cwf | 41 -
.../20110825-14.57-ulf-norells-macbook-pro/functor | 35 -
.../latemeta | 35 -
.../20110825-14.57-ulf-norells-macbook-pro/monad | 36 -
.../monadpostulate | 36 -
.../polyfunctor | 36 -
.../20110825-14.57-ulf-norells-macbook-pro/prim | 35 -
.../20110825-14.57-ulf-norells-macbook-pro/syntax1 | 68 -
.../20110825-14.57-ulf-norells-macbook-pro/syntax2 | 33 -
benchmark/logs/20110830-17.10-dhcp-178109/ac1 | 51 -
benchmark/logs/20110830-17.10-dhcp-178109/ac2 | 53 -
benchmark/logs/20110830-17.10-dhcp-178109/ac3 | 33 -
benchmark/logs/20110830-17.10-dhcp-178109/cat | 35 -
benchmark/logs/20110830-17.10-dhcp-178109/cwf | 41 -
benchmark/logs/20110830-17.10-dhcp-178109/functor | 35 -
benchmark/logs/20110830-17.10-dhcp-178109/latemeta | 35 -
benchmark/logs/20110830-17.10-dhcp-178109/monad | 36 -
.../logs/20110830-17.10-dhcp-178109/monadpostulate | 36 -
.../logs/20110830-17.10-dhcp-178109/polyfunctor | 36 -
benchmark/logs/20110830-17.10-dhcp-178109/prim | 35 -
benchmark/logs/20110830-17.10-dhcp-178109/syntax1 | 68 -
benchmark/logs/20110830-17.10-dhcp-178109/syntax2 | 33 -
benchmark/logs/20110830-18.20-dhcp-178109/ac1 | 51 -
benchmark/logs/20110830-18.20-dhcp-178109/ac2 | 53 -
benchmark/logs/20110830-18.20-dhcp-178109/ac3 | 33 -
benchmark/logs/20110830-18.20-dhcp-178109/cat | 35 -
benchmark/logs/20110830-18.20-dhcp-178109/cwf | 41 -
benchmark/logs/20110830-18.20-dhcp-178109/functor | 35 -
benchmark/logs/20110830-18.20-dhcp-178109/latemeta | 35 -
benchmark/logs/20110830-18.20-dhcp-178109/monad | 36 -
.../logs/20110830-18.20-dhcp-178109/monadpostulate | 36 -
.../logs/20110830-18.20-dhcp-178109/patternmatch | 35 -
.../logs/20110830-18.20-dhcp-178109/polyfunctor | 36 -
benchmark/logs/20110830-18.20-dhcp-178109/prim | 35 -
benchmark/logs/20110830-18.20-dhcp-178109/syntax1 | 68 -
benchmark/logs/20110830-18.20-dhcp-178109/syntax2 | 33 -
benchmark/logs/20110901-08.43-Ulfs-MacBook-Pro/ac1 | 51 -
benchmark/logs/20110901-08.43-Ulfs-MacBook-Pro/ac2 | 53 -
benchmark/logs/20110901-08.43-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110901-08.43-Ulfs-MacBook-Pro/cat | 35 -
benchmark/logs/20110901-08.43-Ulfs-MacBook-Pro/cwf | 41 -
.../logs/20110901-08.43-Ulfs-MacBook-Pro/functor | 35 -
.../logs/20110901-08.43-Ulfs-MacBook-Pro/latemeta | 35 -
.../logs/20110901-08.43-Ulfs-MacBook-Pro/monad | 36 -
.../20110901-08.43-Ulfs-MacBook-Pro/monadpostulate | 36 -
.../20110901-08.43-Ulfs-MacBook-Pro/patternmatch | 35 -
.../20110901-08.43-Ulfs-MacBook-Pro/polyfunctor | 36 -
.../logs/20110901-08.43-Ulfs-MacBook-Pro/prim | 35 -
.../logs/20110901-08.43-Ulfs-MacBook-Pro/syntax1 | 68 -
.../logs/20110901-08.43-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110901-12.30-Ulfs-MacBook-Pro/ac1 | 51 -
benchmark/logs/20110901-12.30-Ulfs-MacBook-Pro/ac2 | 53 -
benchmark/logs/20110901-12.30-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110901-12.30-Ulfs-MacBook-Pro/cat | 35 -
benchmark/logs/20110901-12.30-Ulfs-MacBook-Pro/cwf | 41 -
.../logs/20110901-12.30-Ulfs-MacBook-Pro/functor | 35 -
.../logs/20110901-12.30-Ulfs-MacBook-Pro/latemeta | 35 -
.../logs/20110901-12.30-Ulfs-MacBook-Pro/monad | 36 -
.../20110901-12.30-Ulfs-MacBook-Pro/monadpostulate | 36 -
.../20110901-12.30-Ulfs-MacBook-Pro/patternmatch | 35 -
.../20110901-12.30-Ulfs-MacBook-Pro/polyfunctor | 36 -
.../logs/20110901-12.30-Ulfs-MacBook-Pro/prim | 35 -
.../logs/20110901-12.30-Ulfs-MacBook-Pro/syntax1 | 68 -
.../logs/20110901-12.30-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110901-13.33-Ulfs-MacBook-Pro/ac1 | 51 -
benchmark/logs/20110901-13.33-Ulfs-MacBook-Pro/ac2 | 53 -
benchmark/logs/20110901-13.33-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110901-13.33-Ulfs-MacBook-Pro/cat | 35 -
benchmark/logs/20110901-13.33-Ulfs-MacBook-Pro/cwf | 41 -
.../logs/20110901-13.33-Ulfs-MacBook-Pro/data | 35 -
.../logs/20110901-13.33-Ulfs-MacBook-Pro/functor | 35 -
.../logs/20110901-13.33-Ulfs-MacBook-Pro/latemeta | 35 -
.../logs/20110901-13.33-Ulfs-MacBook-Pro/monad | 36 -
.../20110901-13.33-Ulfs-MacBook-Pro/monadpostulate | 36 -
.../logs/20110901-13.33-Ulfs-MacBook-Pro/nested | 35 -
.../20110901-13.33-Ulfs-MacBook-Pro/patternmatch | 35 -
.../20110901-13.33-Ulfs-MacBook-Pro/polyfunctor | 36 -
.../logs/20110901-13.33-Ulfs-MacBook-Pro/prim | 35 -
.../logs/20110901-13.33-Ulfs-MacBook-Pro/record | 35 -
.../logs/20110901-13.33-Ulfs-MacBook-Pro/syntax1 | 68 -
.../logs/20110901-13.33-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110902-12.38-Ulfs-MacBook-Pro/ac1 | 51 -
benchmark/logs/20110902-12.38-Ulfs-MacBook-Pro/ac2 | 53 -
benchmark/logs/20110902-12.38-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110902-12.38-Ulfs-MacBook-Pro/cat | 35 -
benchmark/logs/20110902-12.38-Ulfs-MacBook-Pro/cwf | 41 -
.../logs/20110902-12.38-Ulfs-MacBook-Pro/data | 35 -
.../logs/20110902-12.38-Ulfs-MacBook-Pro/functor | 35 -
.../logs/20110902-12.38-Ulfs-MacBook-Pro/latemeta | 35 -
.../logs/20110902-12.38-Ulfs-MacBook-Pro/monad | 36 -
.../20110902-12.38-Ulfs-MacBook-Pro/monadpostulate | 36 -
.../logs/20110902-12.38-Ulfs-MacBook-Pro/nested | 35 -
.../20110902-12.38-Ulfs-MacBook-Pro/patternmatch | 35 -
.../20110902-12.38-Ulfs-MacBook-Pro/polyfunctor | 36 -
.../logs/20110902-12.38-Ulfs-MacBook-Pro/prim | 35 -
.../logs/20110902-12.38-Ulfs-MacBook-Pro/record | 35 -
.../logs/20110902-12.38-Ulfs-MacBook-Pro/syntax1 | 68 -
.../logs/20110902-12.38-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110906-12.30-Ulfs-MacBook-Pro/ac1 | 51 -
benchmark/logs/20110906-12.30-Ulfs-MacBook-Pro/ac2 | 53 -
benchmark/logs/20110906-12.30-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110906-12.30-Ulfs-MacBook-Pro/cat | 35 -
benchmark/logs/20110906-12.30-Ulfs-MacBook-Pro/cwf | 41 -
.../logs/20110906-12.30-Ulfs-MacBook-Pro/data | 35 -
.../logs/20110906-12.30-Ulfs-MacBook-Pro/functor | 35 -
.../logs/20110906-12.30-Ulfs-MacBook-Pro/latemeta | 35 -
.../logs/20110906-12.30-Ulfs-MacBook-Pro/monad | 36 -
.../20110906-12.30-Ulfs-MacBook-Pro/monadpostulate | 36 -
.../logs/20110906-12.30-Ulfs-MacBook-Pro/nested | 35 -
.../20110906-12.30-Ulfs-MacBook-Pro/patternmatch | 35 -
.../20110906-12.30-Ulfs-MacBook-Pro/polyfunctor | 36 -
.../logs/20110906-12.30-Ulfs-MacBook-Pro/prim | 35 -
.../logs/20110906-12.30-Ulfs-MacBook-Pro/record | 35 -
.../logs/20110906-12.30-Ulfs-MacBook-Pro/syntax1 | 68 -
.../logs/20110906-12.30-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110907-01.19-Ulfs-MacBook-Pro/ac1 | 51 -
benchmark/logs/20110907-01.19-Ulfs-MacBook-Pro/ac2 | 53 -
benchmark/logs/20110907-01.19-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110907-01.19-Ulfs-MacBook-Pro/cat | 35 -
benchmark/logs/20110907-01.19-Ulfs-MacBook-Pro/cwf | 41 -
.../logs/20110907-01.19-Ulfs-MacBook-Pro/data | 35 -
.../logs/20110907-01.19-Ulfs-MacBook-Pro/functor | 35 -
.../logs/20110907-01.19-Ulfs-MacBook-Pro/latemeta | 35 -
.../logs/20110907-01.19-Ulfs-MacBook-Pro/monad | 36 -
.../20110907-01.19-Ulfs-MacBook-Pro/monadpostulate | 36 -
.../logs/20110907-01.19-Ulfs-MacBook-Pro/nested | 35 -
.../20110907-01.19-Ulfs-MacBook-Pro/patternmatch | 35 -
.../20110907-01.19-Ulfs-MacBook-Pro/polyfunctor | 36 -
.../logs/20110907-01.19-Ulfs-MacBook-Pro/prim | 35 -
.../logs/20110907-01.19-Ulfs-MacBook-Pro/record | 35 -
.../logs/20110907-01.19-Ulfs-MacBook-Pro/syntax1 | 66 -
.../logs/20110907-01.19-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110907-03.11-Ulfs-MacBook-Pro/ac1 | 52 -
benchmark/logs/20110907-03.11-Ulfs-MacBook-Pro/ac2 | 54 -
benchmark/logs/20110907-03.11-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110907-03.11-Ulfs-MacBook-Pro/cat | 35 -
benchmark/logs/20110907-03.11-Ulfs-MacBook-Pro/cwf | 41 -
.../logs/20110907-03.11-Ulfs-MacBook-Pro/data | 35 -
.../logs/20110907-03.11-Ulfs-MacBook-Pro/functor | 36 -
.../logs/20110907-03.11-Ulfs-MacBook-Pro/latemeta | 35 -
.../logs/20110907-03.11-Ulfs-MacBook-Pro/monad | 36 -
.../20110907-03.11-Ulfs-MacBook-Pro/monadpostulate | 36 -
.../logs/20110907-03.11-Ulfs-MacBook-Pro/nested | 35 -
.../20110907-03.11-Ulfs-MacBook-Pro/patternmatch | 35 -
.../20110907-03.11-Ulfs-MacBook-Pro/polyfunctor | 36 -
.../logs/20110907-03.11-Ulfs-MacBook-Pro/prim | 35 -
.../logs/20110907-03.11-Ulfs-MacBook-Pro/record | 35 -
.../logs/20110907-03.11-Ulfs-MacBook-Pro/syntax1 | 68 -
.../logs/20110907-03.11-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110907-03.26-Ulfs-MacBook-Pro/ac1 | 51 -
benchmark/logs/20110907-03.26-Ulfs-MacBook-Pro/ac2 | 53 -
benchmark/logs/20110907-03.26-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110907-03.26-Ulfs-MacBook-Pro/cat | 35 -
benchmark/logs/20110907-03.26-Ulfs-MacBook-Pro/cwf | 41 -
.../logs/20110907-03.26-Ulfs-MacBook-Pro/data | 35 -
.../logs/20110907-03.26-Ulfs-MacBook-Pro/functor | 35 -
.../logs/20110907-03.26-Ulfs-MacBook-Pro/latemeta | 35 -
.../logs/20110907-03.26-Ulfs-MacBook-Pro/monad | 36 -
.../20110907-03.26-Ulfs-MacBook-Pro/monadpostulate | 36 -
.../logs/20110907-03.26-Ulfs-MacBook-Pro/nested | 35 -
.../20110907-03.26-Ulfs-MacBook-Pro/patternmatch | 35 -
.../20110907-03.26-Ulfs-MacBook-Pro/polyfunctor | 36 -
.../logs/20110907-03.26-Ulfs-MacBook-Pro/prim | 35 -
.../logs/20110907-03.26-Ulfs-MacBook-Pro/record | 35 -
.../logs/20110907-03.26-Ulfs-MacBook-Pro/syntax1 | 66 -
.../logs/20110907-03.26-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110907-04.48-Ulfs-MacBook-Pro/ac1 | 51 -
benchmark/logs/20110907-04.48-Ulfs-MacBook-Pro/ac2 | 53 -
benchmark/logs/20110907-04.48-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110907-04.48-Ulfs-MacBook-Pro/cat | 35 -
benchmark/logs/20110907-04.48-Ulfs-MacBook-Pro/cwf | 41 -
.../logs/20110907-04.48-Ulfs-MacBook-Pro/data | 35 -
.../logs/20110907-04.48-Ulfs-MacBook-Pro/functor | 35 -
.../logs/20110907-04.48-Ulfs-MacBook-Pro/latemeta | 35 -
.../logs/20110907-04.48-Ulfs-MacBook-Pro/monad | 36 -
.../20110907-04.48-Ulfs-MacBook-Pro/monadpostulate | 36 -
.../logs/20110907-04.48-Ulfs-MacBook-Pro/nested | 35 -
.../20110907-04.48-Ulfs-MacBook-Pro/patternmatch | 35 -
.../20110907-04.48-Ulfs-MacBook-Pro/polyfunctor | 36 -
.../logs/20110907-04.48-Ulfs-MacBook-Pro/prim | 35 -
.../logs/20110907-04.48-Ulfs-MacBook-Pro/record | 35 -
.../logs/20110907-04.48-Ulfs-MacBook-Pro/syntax1 | 66 -
.../logs/20110907-04.48-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110907-05.32-Ulfs-MacBook-Pro/ac1 | 51 -
benchmark/logs/20110907-05.32-Ulfs-MacBook-Pro/ac2 | 53 -
benchmark/logs/20110907-05.32-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110907-05.32-Ulfs-MacBook-Pro/cat | 35 -
benchmark/logs/20110907-05.32-Ulfs-MacBook-Pro/cwf | 41 -
.../logs/20110907-05.32-Ulfs-MacBook-Pro/data | 35 -
.../logs/20110907-05.32-Ulfs-MacBook-Pro/functor | 35 -
.../logs/20110907-05.32-Ulfs-MacBook-Pro/latemeta | 35 -
.../logs/20110907-05.32-Ulfs-MacBook-Pro/monad | 36 -
.../20110907-05.32-Ulfs-MacBook-Pro/monadpostulate | 36 -
.../logs/20110907-05.32-Ulfs-MacBook-Pro/nested | 35 -
.../20110907-05.32-Ulfs-MacBook-Pro/patternmatch | 35 -
.../20110907-05.32-Ulfs-MacBook-Pro/polyfunctor | 36 -
.../logs/20110907-05.32-Ulfs-MacBook-Pro/prim | 35 -
.../logs/20110907-05.32-Ulfs-MacBook-Pro/record | 35 -
.../logs/20110907-05.32-Ulfs-MacBook-Pro/syntax1 | 66 -
.../logs/20110907-05.32-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110908-14.00-Ulfs-MacBook-Pro/ac1 | 51 -
benchmark/logs/20110908-14.00-Ulfs-MacBook-Pro/ac2 | 53 -
benchmark/logs/20110908-14.00-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110908-14.00-Ulfs-MacBook-Pro/cat | 35 -
benchmark/logs/20110908-14.00-Ulfs-MacBook-Pro/cwf | 41 -
.../logs/20110908-14.00-Ulfs-MacBook-Pro/data | 35 -
.../logs/20110908-14.00-Ulfs-MacBook-Pro/functor | 35 -
.../logs/20110908-14.00-Ulfs-MacBook-Pro/latemeta | 35 -
.../logs/20110908-14.00-Ulfs-MacBook-Pro/monad | 36 -
.../20110908-14.00-Ulfs-MacBook-Pro/monadpostulate | 36 -
.../logs/20110908-14.00-Ulfs-MacBook-Pro/nested | 35 -
.../20110908-14.00-Ulfs-MacBook-Pro/patternmatch | 35 -
.../20110908-14.00-Ulfs-MacBook-Pro/polyfunctor | 36 -
.../logs/20110908-14.00-Ulfs-MacBook-Pro/prim | 35 -
.../logs/20110908-14.00-Ulfs-MacBook-Pro/record | 35 -
.../logs/20110908-14.00-Ulfs-MacBook-Pro/syntax1 | 66 -
.../logs/20110908-14.00-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110909-23.56-Ulfs-MacBook-Pro/ac1 | 61 -
benchmark/logs/20110909-23.56-Ulfs-MacBook-Pro/ac2 | 64 -
benchmark/logs/20110909-23.56-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110909-23.56-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20110909-23.56-Ulfs-MacBook-Pro/cat | 36 -
benchmark/logs/20110909-23.56-Ulfs-MacBook-Pro/cwf | 46 -
.../logs/20110909-23.56-Ulfs-MacBook-Pro/data | 36 -
.../logs/20110909-23.56-Ulfs-MacBook-Pro/functor | 36 -
.../logs/20110909-23.56-Ulfs-MacBook-Pro/latemeta | 36 -
.../logs/20110909-23.56-Ulfs-MacBook-Pro/monad | 38 -
.../20110909-23.56-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20110909-23.56-Ulfs-MacBook-Pro/nested | 36 -
.../20110909-23.56-Ulfs-MacBook-Pro/patternmatch | 36 -
.../20110909-23.56-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20110909-23.56-Ulfs-MacBook-Pro/prim | 36 -
.../logs/20110909-23.56-Ulfs-MacBook-Pro/record | 36 -
.../logs/20110909-23.56-Ulfs-MacBook-Pro/syntax1 | 86 -
.../logs/20110909-23.56-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110910-23.55-Ulfs-MacBook-Pro/ac1 | 61 -
benchmark/logs/20110910-23.55-Ulfs-MacBook-Pro/ac2 | 64 -
benchmark/logs/20110910-23.55-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110910-23.55-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20110910-23.55-Ulfs-MacBook-Pro/cat | 36 -
benchmark/logs/20110910-23.55-Ulfs-MacBook-Pro/cwf | 46 -
.../logs/20110910-23.55-Ulfs-MacBook-Pro/data | 36 -
.../logs/20110910-23.55-Ulfs-MacBook-Pro/functor | 36 -
.../logs/20110910-23.55-Ulfs-MacBook-Pro/latemeta | 36 -
.../logs/20110910-23.55-Ulfs-MacBook-Pro/monad | 38 -
.../20110910-23.55-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20110910-23.55-Ulfs-MacBook-Pro/nested | 36 -
.../20110910-23.55-Ulfs-MacBook-Pro/patternmatch | 36 -
.../20110910-23.55-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20110910-23.55-Ulfs-MacBook-Pro/prim | 36 -
.../logs/20110910-23.55-Ulfs-MacBook-Pro/record | 36 -
.../logs/20110910-23.55-Ulfs-MacBook-Pro/syntax1 | 86 -
.../logs/20110910-23.55-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110915-07.38-Ulfs-MacBook-Pro/ac1 | 67 -
benchmark/logs/20110915-07.38-Ulfs-MacBook-Pro/ac2 | 71 -
benchmark/logs/20110915-07.38-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110915-07.38-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20110915-07.38-Ulfs-MacBook-Pro/cat | 37 -
benchmark/logs/20110915-07.38-Ulfs-MacBook-Pro/cwf | 47 -
.../logs/20110915-07.38-Ulfs-MacBook-Pro/data | 37 -
.../logs/20110915-07.38-Ulfs-MacBook-Pro/functor | 37 -
.../logs/20110915-07.38-Ulfs-MacBook-Pro/latemeta | 37 -
.../logs/20110915-07.38-Ulfs-MacBook-Pro/monad | 38 -
.../20110915-07.38-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20110915-07.38-Ulfs-MacBook-Pro/nested | 37 -
.../20110915-07.38-Ulfs-MacBook-Pro/patternmatch | 37 -
.../20110915-07.38-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20110915-07.38-Ulfs-MacBook-Pro/prim | 37 -
.../logs/20110915-07.38-Ulfs-MacBook-Pro/record | 37 -
.../logs/20110915-07.38-Ulfs-MacBook-Pro/syntax1 | 92 -
.../logs/20110915-07.38-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110915-08.47-Ulfs-MacBook-Pro/ac1 | 67 -
benchmark/logs/20110915-08.47-Ulfs-MacBook-Pro/ac2 | 71 -
benchmark/logs/20110915-08.47-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110915-08.47-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20110915-08.47-Ulfs-MacBook-Pro/cat | 37 -
benchmark/logs/20110915-08.47-Ulfs-MacBook-Pro/cwf | 47 -
.../logs/20110915-08.47-Ulfs-MacBook-Pro/data | 37 -
.../logs/20110915-08.47-Ulfs-MacBook-Pro/functor | 37 -
.../logs/20110915-08.47-Ulfs-MacBook-Pro/latemeta | 37 -
.../logs/20110915-08.47-Ulfs-MacBook-Pro/monad | 38 -
.../20110915-08.47-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20110915-08.47-Ulfs-MacBook-Pro/nested | 37 -
.../20110915-08.47-Ulfs-MacBook-Pro/patternmatch | 37 -
.../20110915-08.47-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20110915-08.47-Ulfs-MacBook-Pro/prim | 37 -
.../logs/20110915-08.47-Ulfs-MacBook-Pro/record | 37 -
.../logs/20110915-08.47-Ulfs-MacBook-Pro/syntax1 | 92 -
.../logs/20110915-08.47-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110915-09.14-Ulfs-MacBook-Pro/ac1 | 67 -
benchmark/logs/20110915-09.14-Ulfs-MacBook-Pro/ac2 | 71 -
benchmark/logs/20110915-09.14-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110915-09.14-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20110915-09.14-Ulfs-MacBook-Pro/cat | 37 -
benchmark/logs/20110915-09.14-Ulfs-MacBook-Pro/cwf | 47 -
.../logs/20110915-09.14-Ulfs-MacBook-Pro/data | 37 -
.../logs/20110915-09.14-Ulfs-MacBook-Pro/functor | 37 -
.../logs/20110915-09.14-Ulfs-MacBook-Pro/latemeta | 37 -
.../logs/20110915-09.14-Ulfs-MacBook-Pro/monad | 38 -
.../20110915-09.14-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20110915-09.14-Ulfs-MacBook-Pro/nested | 37 -
.../20110915-09.14-Ulfs-MacBook-Pro/patternmatch | 37 -
.../20110915-09.14-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20110915-09.14-Ulfs-MacBook-Pro/prim | 37 -
.../logs/20110915-09.14-Ulfs-MacBook-Pro/record | 37 -
.../logs/20110915-09.14-Ulfs-MacBook-Pro/syntax1 | 92 -
.../logs/20110915-09.14-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110915-13.11-Ulfs-MacBook-Pro/ac1 | 67 -
benchmark/logs/20110915-13.11-Ulfs-MacBook-Pro/ac2 | 71 -
benchmark/logs/20110915-13.11-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110915-13.11-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20110915-13.11-Ulfs-MacBook-Pro/cat | 37 -
benchmark/logs/20110915-13.11-Ulfs-MacBook-Pro/cwf | 47 -
.../logs/20110915-13.11-Ulfs-MacBook-Pro/data | 37 -
.../logs/20110915-13.11-Ulfs-MacBook-Pro/functor | 37 -
.../logs/20110915-13.11-Ulfs-MacBook-Pro/latemeta | 37 -
.../logs/20110915-13.11-Ulfs-MacBook-Pro/monad | 38 -
.../20110915-13.11-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20110915-13.11-Ulfs-MacBook-Pro/nested | 37 -
.../20110915-13.11-Ulfs-MacBook-Pro/patternmatch | 37 -
.../20110915-13.11-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20110915-13.11-Ulfs-MacBook-Pro/prim | 37 -
.../logs/20110915-13.11-Ulfs-MacBook-Pro/record | 37 -
.../logs/20110915-13.11-Ulfs-MacBook-Pro/syntax1 | 92 -
.../logs/20110915-13.11-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110919-16.46-Ulfs-MacBook-Pro/ac1 | 67 -
benchmark/logs/20110919-16.46-Ulfs-MacBook-Pro/ac2 | 71 -
benchmark/logs/20110919-16.46-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110919-16.46-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20110919-16.46-Ulfs-MacBook-Pro/cat | 37 -
benchmark/logs/20110919-16.46-Ulfs-MacBook-Pro/cwf | 47 -
.../logs/20110919-16.46-Ulfs-MacBook-Pro/data | 37 -
.../logs/20110919-16.46-Ulfs-MacBook-Pro/functor | 37 -
.../logs/20110919-16.46-Ulfs-MacBook-Pro/latemeta | 37 -
.../logs/20110919-16.46-Ulfs-MacBook-Pro/monad | 38 -
.../20110919-16.46-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20110919-16.46-Ulfs-MacBook-Pro/nested | 37 -
.../20110919-16.46-Ulfs-MacBook-Pro/patternmatch | 37 -
.../20110919-16.46-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20110919-16.46-Ulfs-MacBook-Pro/prim | 37 -
.../logs/20110919-16.46-Ulfs-MacBook-Pro/record | 37 -
.../logs/20110919-16.46-Ulfs-MacBook-Pro/syntax1 | 92 -
.../logs/20110919-16.46-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110922-22.40-Ulfs-MacBook-Pro/ac1 | 67 -
benchmark/logs/20110922-22.40-Ulfs-MacBook-Pro/ac2 | 71 -
benchmark/logs/20110922-22.40-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110922-22.40-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20110922-22.40-Ulfs-MacBook-Pro/cat | 37 -
benchmark/logs/20110922-22.40-Ulfs-MacBook-Pro/cwf | 47 -
.../logs/20110922-22.40-Ulfs-MacBook-Pro/data | 37 -
.../logs/20110922-22.40-Ulfs-MacBook-Pro/functor | 37 -
.../logs/20110922-22.40-Ulfs-MacBook-Pro/latemeta | 37 -
.../logs/20110922-22.40-Ulfs-MacBook-Pro/monad | 38 -
.../20110922-22.40-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20110922-22.40-Ulfs-MacBook-Pro/nested | 37 -
.../20110922-22.40-Ulfs-MacBook-Pro/patternmatch | 37 -
.../20110922-22.40-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20110922-22.40-Ulfs-MacBook-Pro/prim | 37 -
.../logs/20110922-22.40-Ulfs-MacBook-Pro/record | 37 -
.../logs/20110922-22.40-Ulfs-MacBook-Pro/syntax1 | 92 -
.../logs/20110922-22.40-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110924-09.49-Ulfs-MacBook-Pro/ac1 | 67 -
benchmark/logs/20110924-09.49-Ulfs-MacBook-Pro/ac2 | 71 -
benchmark/logs/20110924-09.49-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110924-09.49-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20110924-09.49-Ulfs-MacBook-Pro/cat | 37 -
benchmark/logs/20110924-09.49-Ulfs-MacBook-Pro/cwf | 47 -
.../logs/20110924-09.49-Ulfs-MacBook-Pro/data | 37 -
.../logs/20110924-09.49-Ulfs-MacBook-Pro/functor | 37 -
.../logs/20110924-09.49-Ulfs-MacBook-Pro/latemeta | 37 -
.../logs/20110924-09.49-Ulfs-MacBook-Pro/monad | 38 -
.../20110924-09.49-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20110924-09.49-Ulfs-MacBook-Pro/nested | 37 -
.../20110924-09.49-Ulfs-MacBook-Pro/patternmatch | 37 -
.../20110924-09.49-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20110924-09.49-Ulfs-MacBook-Pro/prim | 37 -
.../logs/20110924-09.49-Ulfs-MacBook-Pro/record | 37 -
.../logs/20110924-09.49-Ulfs-MacBook-Pro/syntax1 | 92 -
.../logs/20110924-09.49-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110924-10.04-Ulfs-MacBook-Pro/ac1 | 67 -
benchmark/logs/20110924-10.04-Ulfs-MacBook-Pro/ac2 | 71 -
benchmark/logs/20110924-10.04-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110924-10.04-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20110924-10.04-Ulfs-MacBook-Pro/cat | 37 -
benchmark/logs/20110924-10.04-Ulfs-MacBook-Pro/cwf | 47 -
.../logs/20110924-10.04-Ulfs-MacBook-Pro/data | 37 -
.../logs/20110924-10.04-Ulfs-MacBook-Pro/functor | 37 -
.../logs/20110924-10.04-Ulfs-MacBook-Pro/latemeta | 37 -
.../logs/20110924-10.04-Ulfs-MacBook-Pro/monad | 38 -
.../20110924-10.04-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20110924-10.04-Ulfs-MacBook-Pro/nested | 37 -
.../20110924-10.04-Ulfs-MacBook-Pro/patternmatch | 37 -
.../20110924-10.04-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20110924-10.04-Ulfs-MacBook-Pro/prim | 37 -
.../logs/20110924-10.04-Ulfs-MacBook-Pro/record | 37 -
.../logs/20110924-10.04-Ulfs-MacBook-Pro/syntax1 | 92 -
.../logs/20110924-10.04-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20110924-10.14-Ulfs-MacBook-Pro/ac1 | 67 -
benchmark/logs/20110924-10.14-Ulfs-MacBook-Pro/ac2 | 71 -
benchmark/logs/20110924-10.14-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20110924-10.14-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20110924-10.14-Ulfs-MacBook-Pro/cat | 37 -
benchmark/logs/20110924-10.14-Ulfs-MacBook-Pro/cwf | 47 -
.../logs/20110924-10.14-Ulfs-MacBook-Pro/data | 37 -
.../logs/20110924-10.14-Ulfs-MacBook-Pro/functor | 37 -
.../logs/20110924-10.14-Ulfs-MacBook-Pro/latemeta | 37 -
.../logs/20110924-10.14-Ulfs-MacBook-Pro/monad | 38 -
.../20110924-10.14-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20110924-10.14-Ulfs-MacBook-Pro/nested | 37 -
.../20110924-10.14-Ulfs-MacBook-Pro/patternmatch | 37 -
.../20110924-10.14-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20110924-10.14-Ulfs-MacBook-Pro/prim | 37 -
.../logs/20110924-10.14-Ulfs-MacBook-Pro/record | 37 -
.../logs/20110924-10.14-Ulfs-MacBook-Pro/syntax1 | 92 -
.../logs/20110924-10.14-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20120216-13.00-Ulfs-MacBook-Pro/ac1 | 67 -
benchmark/logs/20120216-13.00-Ulfs-MacBook-Pro/ac2 | 71 -
benchmark/logs/20120216-13.00-Ulfs-MacBook-Pro/ac3 | 33 -
benchmark/logs/20120216-13.00-Ulfs-MacBook-Pro/any | 38 -
benchmark/logs/20120216-13.00-Ulfs-MacBook-Pro/cat | 37 -
benchmark/logs/20120216-13.00-Ulfs-MacBook-Pro/cwf | 47 -
.../logs/20120216-13.00-Ulfs-MacBook-Pro/data | 37 -
.../logs/20120216-13.00-Ulfs-MacBook-Pro/functor | 37 -
.../logs/20120216-13.00-Ulfs-MacBook-Pro/latemeta | 37 -
.../logs/20120216-13.00-Ulfs-MacBook-Pro/monad | 43 -
.../20120216-13.00-Ulfs-MacBook-Pro/monadpostulate | 38 -
.../logs/20120216-13.00-Ulfs-MacBook-Pro/nested | 37 -
.../20120216-13.00-Ulfs-MacBook-Pro/patternmatch | 37 -
.../20120216-13.00-Ulfs-MacBook-Pro/polyfunctor | 38 -
.../logs/20120216-13.00-Ulfs-MacBook-Pro/prim | 37 -
.../logs/20120216-13.00-Ulfs-MacBook-Pro/record | 37 -
.../logs/20120216-13.00-Ulfs-MacBook-Pro/syntax1 | 92 -
.../logs/20120216-13.00-Ulfs-MacBook-Pro/syntax2 | 33 -
benchmark/logs/20120329-12.19-Ulfs-MacBook-Pro/ac1 | 68 -
benchmark/logs/20120329-12.19-Ulfs-MacBook-Pro/ac2 | 72 -
benchmark/logs/20120329-12.19-Ulfs-MacBook-Pro/ac3 | 34 -
benchmark/logs/20120329-12.19-Ulfs-MacBook-Pro/any | 39 -
benchmark/logs/20120329-12.19-Ulfs-MacBook-Pro/cat | 38 -
benchmark/logs/20120329-12.19-Ulfs-MacBook-Pro/cwf | 48 -
.../logs/20120329-12.19-Ulfs-MacBook-Pro/data | 38 -
.../logs/20120329-12.19-Ulfs-MacBook-Pro/functor | 38 -
.../logs/20120329-12.19-Ulfs-MacBook-Pro/latemeta | 38 -
.../logs/20120329-12.19-Ulfs-MacBook-Pro/monad | 44 -
.../20120329-12.19-Ulfs-MacBook-Pro/monadpostulate | 39 -
.../logs/20120329-12.19-Ulfs-MacBook-Pro/nested | 38 -
.../20120329-12.19-Ulfs-MacBook-Pro/patternmatch | 38 -
.../20120329-12.19-Ulfs-MacBook-Pro/polyfunctor | 39 -
.../logs/20120329-12.19-Ulfs-MacBook-Pro/prim | 38 -
.../logs/20120329-12.19-Ulfs-MacBook-Pro/record | 38 -
.../logs/20120329-12.19-Ulfs-MacBook-Pro/syntax1 | 93 -
.../logs/20120329-12.19-Ulfs-MacBook-Pro/syntax2 | 34 -
benchmark/logs/20120406-10.19-Ulfs-MacBook-Pro/ac1 | 68 -
benchmark/logs/20120406-10.19-Ulfs-MacBook-Pro/ac2 | 72 -
benchmark/logs/20120406-10.19-Ulfs-MacBook-Pro/ac3 | 34 -
benchmark/logs/20120406-10.19-Ulfs-MacBook-Pro/any | 39 -
benchmark/logs/20120406-10.19-Ulfs-MacBook-Pro/cat | 38 -
benchmark/logs/20120406-10.19-Ulfs-MacBook-Pro/cwf | 48 -
.../logs/20120406-10.19-Ulfs-MacBook-Pro/data | 38 -
.../logs/20120406-10.19-Ulfs-MacBook-Pro/functor | 38 -
.../logs/20120406-10.19-Ulfs-MacBook-Pro/latemeta | 38 -
.../logs/20120406-10.19-Ulfs-MacBook-Pro/monad | 44 -
.../20120406-10.19-Ulfs-MacBook-Pro/monadpostulate | 39 -
.../logs/20120406-10.19-Ulfs-MacBook-Pro/nested | 38 -
.../20120406-10.19-Ulfs-MacBook-Pro/patternmatch | 38 -
.../20120406-10.19-Ulfs-MacBook-Pro/polyfunctor | 39 -
.../logs/20120406-10.19-Ulfs-MacBook-Pro/prim | 38 -
.../logs/20120406-10.19-Ulfs-MacBook-Pro/record | 38 -
.../logs/20120406-10.19-Ulfs-MacBook-Pro/syntax1 | 93 -
.../logs/20120406-10.19-Ulfs-MacBook-Pro/syntax2 | 34 -
benchmark/logs/20120509-13.01-Ulfs-MacBook-Pro/ac1 | 68 -
benchmark/logs/20120509-13.01-Ulfs-MacBook-Pro/ac2 | 72 -
benchmark/logs/20120509-13.01-Ulfs-MacBook-Pro/ac3 | 34 -
benchmark/logs/20120509-13.01-Ulfs-MacBook-Pro/any | 39 -
benchmark/logs/20120509-13.01-Ulfs-MacBook-Pro/cat | 38 -
benchmark/logs/20120509-13.01-Ulfs-MacBook-Pro/cwf | 48 -
.../logs/20120509-13.01-Ulfs-MacBook-Pro/data | 38 -
.../logs/20120509-13.01-Ulfs-MacBook-Pro/functor | 38 -
.../logs/20120509-13.01-Ulfs-MacBook-Pro/latemeta | 38 -
.../logs/20120509-13.01-Ulfs-MacBook-Pro/monad | 44 -
.../20120509-13.01-Ulfs-MacBook-Pro/monadpostulate | 39 -
.../logs/20120509-13.01-Ulfs-MacBook-Pro/nested | 38 -
.../20120509-13.01-Ulfs-MacBook-Pro/patternmatch | 38 -
.../20120509-13.01-Ulfs-MacBook-Pro/polyfunctor | 39 -
.../logs/20120509-13.01-Ulfs-MacBook-Pro/prim | 38 -
.../logs/20120509-13.01-Ulfs-MacBook-Pro/record | 38 -
.../logs/20120509-13.01-Ulfs-MacBook-Pro/syntax1 | 93 -
.../logs/20120509-13.01-Ulfs-MacBook-Pro/syntax2 | 34 -
benchmark/logs/20120702-14.40-Ulfs-MacBook-Pro/ac1 | 68 -
benchmark/logs/20120702-14.40-Ulfs-MacBook-Pro/ac2 | 72 -
benchmark/logs/20120702-14.40-Ulfs-MacBook-Pro/ac3 | 34 -
benchmark/logs/20120702-14.40-Ulfs-MacBook-Pro/any | 39 -
benchmark/logs/20120702-14.40-Ulfs-MacBook-Pro/cat | 38 -
benchmark/logs/20120702-14.40-Ulfs-MacBook-Pro/cwf | 48 -
.../logs/20120702-14.40-Ulfs-MacBook-Pro/data | 38 -
.../logs/20120702-14.40-Ulfs-MacBook-Pro/functor | 38 -
.../logs/20120702-14.40-Ulfs-MacBook-Pro/latemeta | 38 -
.../logs/20120702-14.40-Ulfs-MacBook-Pro/monad | 44 -
.../20120702-14.40-Ulfs-MacBook-Pro/monadpostulate | 39 -
.../logs/20120702-14.40-Ulfs-MacBook-Pro/nested | 38 -
.../20120702-14.40-Ulfs-MacBook-Pro/patternmatch | 38 -
.../20120702-14.40-Ulfs-MacBook-Pro/polyfunctor | 39 -
.../logs/20120702-14.40-Ulfs-MacBook-Pro/prim | 38 -
.../logs/20120702-14.40-Ulfs-MacBook-Pro/record | 38 -
.../logs/20120702-14.40-Ulfs-MacBook-Pro/syntax1 | 93 -
.../logs/20120702-14.40-Ulfs-MacBook-Pro/syntax2 | 34 -
benchmark/logs/20120705-07.39-Ulfs-MacBook-Pro/ac1 | 68 -
benchmark/logs/20120705-07.39-Ulfs-MacBook-Pro/ac2 | 72 -
benchmark/logs/20120705-07.39-Ulfs-MacBook-Pro/ac3 | 34 -
benchmark/logs/20120705-07.39-Ulfs-MacBook-Pro/any | 39 -
benchmark/logs/20120705-07.39-Ulfs-MacBook-Pro/cat | 38 -
benchmark/logs/20120705-07.39-Ulfs-MacBook-Pro/cwf | 48 -
.../logs/20120705-07.39-Ulfs-MacBook-Pro/data | 38 -
.../logs/20120705-07.39-Ulfs-MacBook-Pro/functor | 38 -
.../logs/20120705-07.39-Ulfs-MacBook-Pro/latemeta | 38 -
.../logs/20120705-07.39-Ulfs-MacBook-Pro/monad | 44 -
.../20120705-07.39-Ulfs-MacBook-Pro/monadpostulate | 39 -
.../logs/20120705-07.39-Ulfs-MacBook-Pro/nested | 38 -
.../20120705-07.39-Ulfs-MacBook-Pro/patternmatch | 38 -
.../20120705-07.39-Ulfs-MacBook-Pro/polyfunctor | 39 -
.../logs/20120705-07.39-Ulfs-MacBook-Pro/prim | 38 -
.../logs/20120705-07.39-Ulfs-MacBook-Pro/record | 38 -
.../logs/20120705-07.39-Ulfs-MacBook-Pro/syntax1 | 93 -
.../logs/20120705-07.39-Ulfs-MacBook-Pro/syntax2 | 34 -
benchmark/logs/20121005-18.37-Ulfs-MacBook-Pro/ac1 | 84 -
benchmark/logs/20121005-18.37-Ulfs-MacBook-Pro/ac2 | 90 -
benchmark/logs/20121005-18.37-Ulfs-MacBook-Pro/ac3 | 34 -
benchmark/logs/20121005-18.37-Ulfs-MacBook-Pro/any | 42 -
benchmark/logs/20121005-18.37-Ulfs-MacBook-Pro/cat | 40 -
benchmark/logs/20121005-18.37-Ulfs-MacBook-Pro/cwf | 55 -
.../logs/20121005-18.37-Ulfs-MacBook-Pro/data | 41 -
.../logs/20121005-18.37-Ulfs-MacBook-Pro/functor | 40 -
.../logs/20121005-18.37-Ulfs-MacBook-Pro/latemeta | 40 -
.../logs/20121005-18.37-Ulfs-MacBook-Pro/monad | 48 -
.../20121005-18.37-Ulfs-MacBook-Pro/monadpostulate | 42 -
.../logs/20121005-18.37-Ulfs-MacBook-Pro/nested | 41 -
.../20121005-18.37-Ulfs-MacBook-Pro/patternmatch | 40 -
.../20121005-18.37-Ulfs-MacBook-Pro/polyfunctor | 41 -
.../logs/20121005-18.37-Ulfs-MacBook-Pro/prim | 41 -
.../logs/20121005-18.37-Ulfs-MacBook-Pro/record | 41 -
.../logs/20121005-18.37-Ulfs-MacBook-Pro/syntax1 | 120 -
.../logs/20121005-18.37-Ulfs-MacBook-Pro/syntax2 | 34 -
benchmark/logs/20121005-20.31-Ulfs-MacBook-Pro/ac1 | 84 -
benchmark/logs/20121005-20.31-Ulfs-MacBook-Pro/ac2 | 90 -
benchmark/logs/20121005-20.31-Ulfs-MacBook-Pro/ac3 | 34 -
benchmark/logs/20121005-20.31-Ulfs-MacBook-Pro/any | 41 -
benchmark/logs/20121005-20.31-Ulfs-MacBook-Pro/cat | 40 -
benchmark/logs/20121005-20.31-Ulfs-MacBook-Pro/cwf | 54 -
.../logs/20121005-20.31-Ulfs-MacBook-Pro/data | 40 -
.../logs/20121005-20.31-Ulfs-MacBook-Pro/functor | 40 -
.../logs/20121005-20.31-Ulfs-MacBook-Pro/latemeta | 40 -
.../logs/20121005-20.31-Ulfs-MacBook-Pro/monad | 48 -
.../20121005-20.31-Ulfs-MacBook-Pro/monadpostulate | 41 -
.../logs/20121005-20.31-Ulfs-MacBook-Pro/nested | 40 -
.../20121005-20.31-Ulfs-MacBook-Pro/patternmatch | 40 -
.../20121005-20.31-Ulfs-MacBook-Pro/polyfunctor | 41 -
.../logs/20121005-20.31-Ulfs-MacBook-Pro/prim | 40 -
.../logs/20121005-20.31-Ulfs-MacBook-Pro/record | 40 -
.../logs/20121005-20.31-Ulfs-MacBook-Pro/syntax1 | 119 -
.../logs/20121005-20.31-Ulfs-MacBook-Pro/syntax2 | 34 -
benchmark/misc/Coverage.agda | 22 -
benchmark/misc/Functor.agda | 64 -
benchmark/misc/FunctorComposition.agda | 27 -
benchmark/misc/LateMetaVariableInstantiation.agda | 39 -
benchmark/misc/UniversePolymorphicFunctor.agda | 88 -
benchmark/monad/IndexedMap.agda | 12 -
benchmark/monad/Monad.agda | 226 -
benchmark/monad/MonadPostulates.agda | 229 -
benchmark/notes | 86 -
benchmark/proj/Data.agda | 57 -
benchmark/proj/Nested.agda | 59 -
benchmark/proj/Record.agda | 65 -
benchmark/std-lib/Any.agda | 622 --
benchmark/tests.mk | 50 -
configure.ac | 50 -
dist/build/Agda/Syntax/Parser/Lexer.hs | 464 ++
dist/build/Agda/Syntax/Parser/Parser.hs | 5595 ++++++++++++++++
doc/HCAR/December-2007.tex | 33 -
doc/HCAR/May-2008.tex | 41 -
doc/HCAR/May-2009.tex | 46 -
doc/HCAR/May-2010.tex | 37 -
doc/HCAR/May-2011.tex | 36 -
doc/HCAR/May-2012.tex | 41 -
doc/HCAR/November-2008.tex | 51 -
doc/HCAR/November-2009.tex | 38 -
doc/HCAR/November-2010.tex | 38 -
doc/HCAR/November-2011.tex | 41 -
doc/HCAR/November-2012.tex | 38 -
doc/haddock/.cvsignore | 4 -
doc/haddock/Makefile | 148 -
doc/haddock/prologue | 1 -
doc/pfe/.cvsignore | 1 -
doc/pfe/fake/Data/Generics.hs | 20 -
doc/pfe/fake/Data/Map.hs | 2 -
doc/pfe/fake/Syntax/Parser/.cvsignore | 1 -
doc/pfe/pfe.txt | 57 -
doc/release-notes/2-2-0.txt | 102 -
doc/release-notes/2-2-10.txt | 214 -
doc/release-notes/2-2-2.txt | 23 -
doc/release-notes/2-2-4.txt | 47 -
doc/release-notes/2-2-6.txt | 257 -
doc/release-notes/2-2-8.txt | 564 --
doc/release-notes/2-3-0.txt | 1005 ---
doc/release-notes/2-3-2-1.txt | 18 -
doc/release-notes/2-3-2-2.txt | 10 -
doc/release-notes/2-3-2.txt | 699 --
examples/.cvsignore | 4 -
examples/AIM4/bag/.cvsignore | 4 -
examples/AIM4/bag/Bag.agda | 270 -
examples/AIM4/bag/Datoid.agda | 47 -
examples/AIM4/bag/Eq.agda | 21 -
examples/AIM4/bag/Equiv.agda | 116 -
examples/AIM4/bag/List.agda | 95 -
examples/AIM4/bag/Nat.agda | 53 -
examples/AIM4/bag/ParserC.agda | 95 -
examples/AIM4/bag/Pos.agda | 56 -
examples/AIM4/bag/Prelude.agda | 95 -
examples/AIM5/Hedberg/SET.agda | 601 --
examples/AIM5/PolyDep/.cvsignore | 1 -
examples/AIM5/PolyDep/EqBase.agda | 121 -
examples/AIM5/PolyDep/Homogenous/.cvsignore | 1 -
examples/AIM5/PolyDep/Homogenous/Base.agda | 140 -
examples/AIM5/PolyDep/Homogenous/Equality.agda | 41 -
examples/AIM5/PolyDep/Homogenous/Nat.agda | 34 -
examples/AIM5/PolyDep/Homogenous/Reflexivity.agda | 53 -
examples/AIM5/PolyDep/Main.agda | 12 -
examples/AIM5/PolyDep/PolyDepPrelude.agda | 160 -
examples/AIM5/PolyDep/Reflexivity.agda | 13 -
examples/AIM5/PolyDep/TYPE.agda | 8 -
examples/AIM5/PolyDep/Tools.agda | 299 -
examples/AIM5/PolyDep/log.txt | 16 -
examples/AIM5/yoshiki/.cvsignore | 4 -
examples/AIM5/yoshiki/SET.agda | 497 --
examples/AIM6/HelloAgda/Basics.agda | 96 -
examples/AIM6/HelloAgda/Bool.agda | 10 -
examples/AIM6/HelloAgda/Datatypes.agda | 108 -
examples/AIM6/HelloAgda/Everything.agda | 10 -
examples/AIM6/HelloAgda/Families.agda | 119 -
examples/AIM6/HelloAgda/Modules.agda | 173 -
examples/AIM6/HelloAgda/Naturals.agda | 23 -
examples/AIM6/HelloAgda/Records.agda | 127 -
examples/AIM6/HelloAgda/With.agda | 84 -
examples/AIM6/HelloAgda/outline | 29 -
examples/AIM6/Path/All.agda | 14 -
examples/AIM6/Path/Elem.agda | 8 -
examples/AIM6/Path/Examples.agda | 48 -
examples/AIM6/Path/Fin.agda | 16 -
examples/AIM6/Path/Lambda.agda | 117 -
examples/AIM6/Path/List.agda | 16 -
examples/AIM6/Path/MapTm.agda | 39 -
examples/AIM6/Path/Modal.agda | 65 -
examples/AIM6/Path/Nat.agda | 31 -
examples/AIM6/Path/Prelude.agda | 88 -
examples/AIM6/Path/Span.agda | 57 -
examples/AIM6/Path/Star.agda | 74 -
examples/AIM6/Path/Vec.agda | 45 -
examples/AIM6/RegExp/talk/BoolMatcher.agda | 46 -
examples/AIM6/RegExp/talk/Eq.agda | 43 -
examples/AIM6/RegExp/talk/Everything.agda | 8 -
examples/AIM6/RegExp/talk/Prelude.agda | 67 -
examples/AIM6/RegExp/talk/RegExps.agda | 73 -
examples/AIM6/RegExp/talk/Setoids.agda | 18 -
examples/AIM6/RegExp/talk/SimpleMatcher.agda | 62 -
examples/AIM6/RegExp/talk/TALK | 68 -
examples/Binary.agda | 53 -
examples/ISWIM.agda | 156 -
examples/Introduction/.cvsignore | 3 -
examples/Introduction/All.agda | 14 -
examples/Introduction/Basics.agda | 126 -
examples/Introduction/Built-in.agda | 162 -
examples/Introduction/Data/.cvsignore | 2 -
examples/Introduction/Data/ByRecursion.agda | 35 -
examples/Introduction/Data/Empty.agda | 41 -
examples/Introduction/Data/Parameterised.agda | 45 -
examples/Introduction/Data/Vec.agda | 35 -
examples/Introduction/Implicit.agda | 110 -
examples/Introduction/Modules.agda | 123 -
examples/Introduction/Modules/.cvsignore | 3 -
examples/Introduction/Modules/Parameterised.agda | 64 -
examples/Introduction/Operators.agda | 65 -
examples/Introduction/Unicode.agda | 36 -
examples/Introduction/Universes.agda | 12 -
examples/Lookup.agda | 49 -
examples/Makefile | 190 -
examples/Miller/Pat.agda | 33 -
examples/Monad.agda | 94 -
examples/ParenDepTac.agda | 235 -
examples/Setoid.agda | 317 -
examples/SimpleTypes.agda | 173 -
examples/SummerSchool07/Lecture/Basics.agda | 90 -
examples/SummerSchool07/Lecture/Bool.agda | 10 -
examples/SummerSchool07/Lecture/CurryHoward.agda | 49 -
examples/SummerSchool07/Lecture/Datatypes.agda | 100 -
examples/SummerSchool07/Lecture/Families.agda | 112 -
examples/SummerSchool07/Lecture/Filter.agda | 52 -
examples/SummerSchool07/Lecture/Modules.agda | 145 -
examples/SummerSchool07/Lecture/Nat.agda | 24 -
examples/SummerSchool07/Lecture/Parity.agda | 37 -
examples/SummerSchool07/Lecture/Records.agda | 128 -
examples/SummerSchool07/Solutions/Problem1.agda | 48 -
examples/SummerSchool07/Solutions/Problem2.agda | 35 -
examples/SummerSchool07/Solutions/Problem3.agda | 37 -
examples/SummerSchool07/Solutions/Problem4.agda | 157 -
examples/TT.agda | 500 --
examples/Termination/Acc.agda | 51 -
examples/Termination/Common/Coinduction.agda | 14 -
examples/Termination/Common/Level.agda | 15 -
examples/Termination/Example.agda | 320 -
examples/Termination/List.agda | 147 -
examples/Termination/Mutual.agda | 21 -
examples/Termination/Nat.agda | 91 -
examples/Termination/Ord.agda | 15 -
examples/Termination/README | 1 -
examples/Termination/Sized/DeBruijn.agda | 240 -
.../Termination/Sized/DeBruijnExSubstSized.agda | 98 -
examples/Termination/Sized/SizedNat.agda | 44 -
examples/Termination/Sized/SizedNatAnnotated.agda | 21 -
examples/Termination/Stream.agda | 57 -
examples/Termination/StreamEating.agda | 44 -
examples/Termination/StreamProc.agda | 70 -
examples/Termination/StructuralOrder.agda | 36 -
.../Termination/TerminationTwoConstructors.agda | 21 -
examples/Termination/Tuple.agda | 36 -
examples/Termination/Where.agda | 23 -
examples/Termination/comb.agda | 88 -
examples/Termination/simplified-comb.agda | 21 -
examples/Vec.agda | 167 -
examples/arith/DivMod.agda | 101 -
...ed-according-to-the-Haskell-lexical-syntax.agda | 18 -
examples/compiler/main.agda | 12 -
examples/instance-arguments/01-arguments.agda | 32 -
examples/instance-arguments/02-classes-indep.agda | 61 -
examples/instance-arguments/03-classes.agda | 53 -
examples/instance-arguments/04-equality.agda | 95 -
examples/instance-arguments/05-equality-std1.agda | 19 -
examples/instance-arguments/05-equality-std2.agda | 15 -
examples/instance-arguments/06-listEquality.agda | 51 -
examples/instance-arguments/07-subclasses.agda | 134 -
examples/instance-arguments/08-higherOrder.agda | 12 -
.../instance-arguments/09-higherOrderClasses.agda | 19 -
examples/instance-arguments/10-localInstances.agda | 32 -
examples/instance-arguments/11-monads.agda | 69 -
.../instance-arguments/12-constraintFamilies.agda | 37 -
.../13-implicitProofObligations.agda | 45 -
.../14-implicitConfigurations.agda | 54 -
examples/lib/.cvsignore | 4 -
examples/lib/Data/.cvsignore | 4 -
examples/lib/Data/Bits.agda | 47 -
examples/lib/Data/Bool.agda | 58 -
examples/lib/Data/Char.agda | 7 -
examples/lib/Data/Fin.agda | 93 -
examples/lib/Data/Integer.agda | 106 -
examples/lib/Data/Interval.agda | 12 -
examples/lib/Data/List.agda | 66 -
examples/lib/Data/Map.agda | 48 -
examples/lib/Data/Maybe.agda | 11 -
examples/lib/Data/Nat.agda | 103 -
examples/lib/Data/Nat/.cvsignore | 4 -
examples/lib/Data/Nat/Properties.agda | 127 -
examples/lib/Data/Permutation.agda | 133 -
examples/lib/Data/PigeonHole.agda | 63 -
examples/lib/Data/Rational.agda | 102 -
examples/lib/Data/Real/.cvsignore | 4 -
examples/lib/Data/Real/Base.agda | 52 -
examples/lib/Data/Real/CReal.agda | 220 -
examples/lib/Data/Real/Complete.agda | 54 -
examples/lib/Data/Real/Gauge.agda | 8 -
examples/lib/Data/Show.agda | 41 -
examples/lib/Data/String.agda | 24 -
examples/lib/Data/Tuple.agda | 12 -
examples/lib/Data/Vec.agda | 105 -
examples/lib/Logic/.cvsignore | 4 -
examples/lib/Logic/Base.agda | 41 -
examples/lib/Logic/ChainReasoning.agda | 84 -
examples/lib/Logic/Congruence.agda | 52 -
examples/lib/Logic/Equivalence.agda | 13 -
examples/lib/Logic/Identity.agda | 40 -
examples/lib/Logic/Leibniz.agda | 19 -
examples/lib/Logic/Operations.agda | 45 -
examples/lib/Logic/Relations.agda | 42 -
examples/lib/Logic/Structure/.cvsignore | 4 -
examples/lib/Logic/Structure/Applicative.agda | 24 -
examples/lib/Logic/Structure/Monoid.agda | 45 -
examples/lib/Prelude.agda | 27 -
examples/lib/Test.agda | 37 -
examples/malformed/Empty.agda | 1 -
examples/order/.cvsignore | 4 -
examples/order/DecidableOrder.agda | 19 -
examples/order/MinMax.agda | 150 -
.../outdated-and-incorrect/AIM6/Cat/Category.agda | 49 -
.../outdated-and-incorrect/AIM6/Cat/Functor.agda | 15 -
.../outdated-and-incorrect/AIM6/Cat/Pullback.agda | 27 -
.../outdated-and-incorrect/AIM6/Cat/Setoid.agda | 71 -
.../outdated-and-incorrect/AIM6/Cat/Slice.agda | 91 -
.../outdated-and-incorrect/AIM6/Cat/Unique.agda | 38 -
.../outdated-and-incorrect/AIM6/Cat/lib/.cvsignore | 0
.../AIM6/Cat/lib/Data/Bits.agda | 46 -
.../AIM6/Cat/lib/Data/Bool.agda | 58 -
.../AIM6/Cat/lib/Data/Char.agda | 7 -
.../AIM6/Cat/lib/Data/Fin.agda | 93 -
.../AIM6/Cat/lib/Data/Integer.agda | 105 -
.../AIM6/Cat/lib/Data/Interval.agda | 12 -
.../AIM6/Cat/lib/Data/List.agda | 66 -
.../AIM6/Cat/lib/Data/Map.agda | 45 -
.../AIM6/Cat/lib/Data/Maybe.agda | 8 -
.../AIM6/Cat/lib/Data/Nat.agda | 102 -
.../AIM6/Cat/lib/Data/Nat/.cvsignore | 4 -
.../AIM6/Cat/lib/Data/Nat/Properties.agda | 127 -
.../AIM6/Cat/lib/Data/Permutation.agda | 130 -
.../AIM6/Cat/lib/Data/PigeonHole.agda | 63 -
.../AIM6/Cat/lib/Data/Rational.agda | 101 -
.../AIM6/Cat/lib/Data/Real/.cvsignore | 4 -
.../AIM6/Cat/lib/Data/Real/Base.agda | 52 -
.../AIM6/Cat/lib/Data/Real/CReal.agda | 219 -
.../AIM6/Cat/lib/Data/Real/Complete.agda | 54 -
.../AIM6/Cat/lib/Data/Real/Gauge.agda | 8 -
.../AIM6/Cat/lib/Data/Show.agda | 40 -
.../AIM6/Cat/lib/Data/String.agda | 24 -
.../AIM6/Cat/lib/Data/Tuple.agda | 12 -
.../AIM6/Cat/lib/Data/Vec.agda | 102 -
.../AIM6/Cat/lib/Logic/.cvsignore | 4 -
.../AIM6/Cat/lib/Logic/Base.agda | 41 -
.../AIM6/Cat/lib/Logic/ChainReasoning.agda | 84 -
.../AIM6/Cat/lib/Logic/Congruence.agda | 52 -
.../AIM6/Cat/lib/Logic/Equivalence.agda | 13 -
.../AIM6/Cat/lib/Logic/Identity.agda | 40 -
.../AIM6/Cat/lib/Logic/Leibniz.agda | 19 -
.../AIM6/Cat/lib/Logic/Operations.agda | 45 -
.../AIM6/Cat/lib/Logic/Relations.agda | 42 -
.../AIM6/Cat/lib/Logic/Structure/.cvsignore | 4 -
.../AIM6/Cat/lib/Logic/Structure/Applicative.agda | 24 -
.../AIM6/Cat/lib/Logic/Structure/Monoid.agda | 45 -
.../AIM6/Cat/lib/Prelude.agda | 27 -
.../outdated-and-incorrect/AIM6/Cat/lib/Test.agda | 33 -
.../Alonzo/AlonzoPrelude.agda | 79 -
.../outdated-and-incorrect/Alonzo/BadPrintf.agda | 85 -
.../outdated-and-incorrect/Alonzo/BadPrintf2.agda | 82 -
examples/outdated-and-incorrect/Alonzo/Bool.agda | 10 -
examples/outdated-and-incorrect/Alonzo/Bool.hs | 19 -
.../outdated-and-incorrect/Alonzo/ListTest.agda | 14 -
examples/outdated-and-incorrect/Alonzo/Makefile | 35 -
examples/outdated-and-incorrect/Alonzo/Point.agda | 14 -
examples/outdated-and-incorrect/Alonzo/Point.hs | 20 -
.../outdated-and-incorrect/Alonzo/PreludeAll.agda | 8 -
.../outdated-and-incorrect/Alonzo/PreludeBool.agda | 48 -
.../outdated-and-incorrect/Alonzo/PreludeInt.agda | 25 -
.../outdated-and-incorrect/Alonzo/PreludeList.agda | 65 -
.../outdated-and-incorrect/Alonzo/PreludeNat.agda | 92 -
.../Alonzo/PreludeNatType.agda | 9 -
.../Alonzo/PreludeNatType.hs | 13 -
.../outdated-and-incorrect/Alonzo/PreludeShow.agda | 62 -
.../Alonzo/PreludeString.agda | 34 -
.../outdated-and-incorrect/Alonzo/Primitive.agda | 2 -
.../outdated-and-incorrect/Alonzo/PrintFloat.agda | 81 -
.../outdated-and-incorrect/Alonzo/PrintNat.agda | 6 -
examples/outdated-and-incorrect/Alonzo/Printf.agda | 83 -
examples/outdated-and-incorrect/Alonzo/Proj.agda | 20 -
examples/outdated-and-incorrect/Alonzo/Q.agda | 33 -
examples/outdated-and-incorrect/Alonzo/README | 38 -
examples/outdated-and-incorrect/Alonzo/RTD.hs | 10 -
examples/outdated-and-incorrect/Alonzo/RTN.agda | 9 -
examples/outdated-and-incorrect/Alonzo/RTN.hs | 13 -
examples/outdated-and-incorrect/Alonzo/RTP.agda | 42 -
examples/outdated-and-incorrect/Alonzo/RTP.hs | 91 -
examples/outdated-and-incorrect/Alonzo/RTP.hs.sav | 49 -
examples/outdated-and-incorrect/Alonzo/RTS.hs | 9 -
.../outdated-and-incorrect/Alonzo/Records.agda | 128 -
examples/outdated-and-incorrect/Alonzo/Records.hs | 122 -
.../outdated-and-incorrect/Alonzo/TestInt.agda | 7 -
.../outdated-and-incorrect/Alonzo/TestNat.agda | 24 -
.../outdated-and-incorrect/Alonzo/TestVec.agda | 20 -
.../outdated-and-incorrect/Alonzo/TestWith.agda | 88 -
examples/outdated-and-incorrect/Alonzo/Vec.agda | 168 -
examples/outdated-and-incorrect/Alonzo/almake | 4 -
.../DTP08/conor/SomeBasicStuff.agda | 55 -
.../outdated-and-incorrect/DTP08/conor/Talk.agda | 169 -
.../outdated-and-incorrect/DTP08/ulf/Talk.agda | 85 -
.../outdated-and-incorrect/FunctionsInIndices.agda | 44 -
examples/outdated-and-incorrect/IORef.agda | 215 -
examples/outdated-and-incorrect/NBE.agda | 397 --
.../NestedDataTypes/DeBruijn.agda | 105 -
.../NestedDataTypes/DeBruijnExSubst.agda | 90 -
.../NestedDataTypes/DeBruijnExSubstSized.agda | 83 -
examples/outdated-and-incorrect/OTT/ObsEq.agda | 323 -
examples/outdated-and-incorrect/OTT/ObsEq2.agda | 295 -
examples/outdated-and-incorrect/ProofRep.agda | 42 -
examples/outdated-and-incorrect/README | 3 -
examples/outdated-and-incorrect/Screen.agda | 69 -
examples/outdated-and-incorrect/StackLanguage.agda | 39 -
examples/outdated-and-incorrect/Subset.agda | 35 -
examples/outdated-and-incorrect/Warshall.agda | 120 -
examples/outdated-and-incorrect/cat/.cvsignore | 4 -
examples/outdated-and-incorrect/cat/Adjoint.agda | 31 -
examples/outdated-and-incorrect/cat/Base.agda | 11 -
examples/outdated-and-incorrect/cat/Category.agda | 132 -
examples/outdated-and-incorrect/cat/Dual.agda | 35 -
examples/outdated-and-incorrect/cat/Example.agda | 100 -
examples/outdated-and-incorrect/cat/Functor.agda | 99 -
examples/outdated-and-incorrect/cat/Iso.agda | 12 -
examples/outdated-and-incorrect/cat/Product.agda | 42 -
examples/outdated-and-incorrect/cat/Terminal.agda | 40 -
examples/outdated-and-incorrect/cat/Unique.agda | 38 -
examples/outdated-and-incorrect/cbs/Basics.agda | 84 -
examples/outdated-and-incorrect/cbs/Graph.agda | 19 -
examples/outdated-and-incorrect/cbs/Hear.agda | 48 -
examples/outdated-and-incorrect/cbs/Interp.agda | 54 -
examples/outdated-and-incorrect/cbs/Mission.agda | 89 -
examples/outdated-and-incorrect/cbs/Path.agda | 122 -
examples/outdated-and-incorrect/cbs/Proc.agda | 174 -
examples/outdated-and-incorrect/cbs/Proof.agda | 132 -
examples/outdated-and-incorrect/cbs/Silence.agda | 48 -
examples/outdated-and-incorrect/cbs/Star.agda | 6 -
examples/outdated-and-incorrect/clowns/.cvsignore | 4 -
.../outdated-and-incorrect/clowns/ChainRule.agda | 73 -
examples/outdated-and-incorrect/clowns/Clowns.agda | 66 -
.../outdated-and-incorrect/clowns/Derivative.agda | 24 -
.../outdated-and-incorrect/clowns/Dissect.agda | 115 -
.../outdated-and-incorrect/clowns/Equality.agda | 28 -
.../outdated-and-incorrect/clowns/Functor.agda | 61 -
.../outdated-and-incorrect/clowns/Isomorphism.agda | 49 -
examples/outdated-and-incorrect/clowns/Sets.agda | 66 -
examples/outdated-and-incorrect/clowns/Zipper.agda | 21 -
examples/outdated-and-incorrect/fileIO/Base.agda | 37 -
examples/outdated-and-incorrect/fileIO/IO.agda | 22 -
.../outdated-and-incorrect/fileIO/IO/File.agda | 115 -
examples/outdated-and-incorrect/fileIO/Main.agda | 33 -
examples/outdated-and-incorrect/fileIO/Makefile | 7 -
examples/outdated-and-incorrect/iird/.cvsignore | 4 -
.../iird/DefinitionalEquality.agda | 72 -
examples/outdated-and-incorrect/iird/Dummy.agda | 2 -
examples/outdated-and-incorrect/iird/Examples.agda | 46 -
.../iird/IID-New-Proof-Setup.agda | 26 -
.../iird/IID-Proof-Setup.agda | 130 -
.../iird/IID-Proof-Test.agda | 63 -
.../outdated-and-incorrect/iird/IID-Proof.agda | 136 -
examples/outdated-and-incorrect/iird/IID.agda | 90 -
examples/outdated-and-incorrect/iird/IIDg.agda | 50 -
examples/outdated-and-incorrect/iird/IIDr.agda | 28 -
examples/outdated-and-incorrect/iird/IIRD.agda | 133 -
examples/outdated-and-incorrect/iird/IIRDg.agda | 127 -
examples/outdated-and-incorrect/iird/IIRDr.agda | 29 -
examples/outdated-and-incorrect/iird/Identity.agda | 46 -
examples/outdated-and-incorrect/iird/LF.agda | 54 -
.../iird/Logic/ChainReasoning.agda | 84 -
examples/outdated-and-incorrect/iird/Main.agda | 5 -
examples/outdated-and-incorrect/iird/Proof.agda | 130 -
.../outdated-and-incorrect/iird/Proof/.cvsignore | 4 -
.../outdated-and-incorrect/iird/Proof/Setup.agda | 153 -
examples/outdated-and-incorrect/iird/Test.agda | 24 -
examples/outdated-and-incorrect/iird/new/IID.agda | 149 -
examples/outdated-and-incorrect/lattice/Chain.agda | 21 -
.../outdated-and-incorrect/lattice/Lattice.agda | 96 -
.../lattice/PartialOrder.agda | 59 -
.../outdated-and-incorrect/lattice/Prelude.agda | 29 -
.../lattice/SemiLattice.agda | 99 -
.../outdated-and-incorrect/syntax/ModuleA.agda | 16 -
.../outdated-and-incorrect/syntax/ModuleB.agda | 35 -
examples/outdated-and-incorrect/syntax/Syntax.agda | 427 --
.../outdated-and-incorrect/tactics/bool/All.agda | 46 -
.../outdated-and-incorrect/tactics/bool/Bool.agda | 82 -
.../outdated-and-incorrect/tactics/bool/Vec.agda | 21 -
examples/outdated-and-incorrect/tait/Chain.agda | 24 -
examples/outdated-and-incorrect/tait/Lambda.agda | 53 -
examples/outdated-and-incorrect/tait/Prelude.agda | 106 -
examples/outdated-and-incorrect/tait/Proof.agda | 101 -
.../outdated-and-incorrect/tait/Reduction.agda | 29 -
examples/outdated-and-incorrect/tait/Subst.agda | 188 -
examples/outdated-and-incorrect/tait/Trans.agda | 44 -
examples/outdated-and-incorrect/univ/.cvsignore | 2 -
examples/outdated-and-incorrect/univ/Base.agda | 31 -
examples/outdated-and-incorrect/univ/Example.agda | 23 -
examples/outdated-and-incorrect/univ/Main.agda | 8 -
examples/outdated-and-incorrect/univ/Nat.agda | 33 -
examples/outdated-and-incorrect/univ/bugs-in-paper | 3 -
examples/outdated-and-incorrect/univ/cwf.agda | 288 -
examples/outdated-and-incorrect/univ/help.agda | 60 -
examples/outdated-and-incorrect/univ/proofs.agda | 125 -
examples/outdated-and-incorrect/univ/tmp.agda | 31 -
examples/outdated-and-incorrect/univ/univ.agda | 379 --
examples/relocatable/originals/A.agda | 3 -
examples/relocatable/originals/B.agda | 6 -
examples/relocatable/originals/C.agda | 6 -
examples/simple-lib/Lib/Bool.agda | 51 -
examples/simple-lib/Lib/Eq.agda | 50 -
examples/simple-lib/Lib/Fin.agda | 80 -
examples/simple-lib/Lib/IO.agda | 42 -
examples/simple-lib/Lib/Id.agda | 12 -
examples/simple-lib/Lib/List.agda | 83 -
examples/simple-lib/Lib/Logic.agda | 19 -
examples/simple-lib/Lib/Maybe.agda | 9 -
examples/simple-lib/Lib/Monad.agda | 154 -
examples/simple-lib/Lib/Nat.agda | 53 -
examples/simple-lib/Lib/Prelude.agda | 35 -
examples/simple-lib/Lib/Vec.agda | 40 -
examples/simple-lib/TestLib.agda | 16 -
examples/sinatra/Example.agda | 54 -
examples/sinatra/Prelude.agda | 28 -
examples/sinatra/Typed.agda | 119 -
examples/syntax/.cvsignore | 2 -
examples/syntax/Literate.lagda | 31 -
examples/syntax/highlighting/.cvsignore | 4 -
examples/syntax/highlighting/Test.agda | 100 -
examples/syntax/highlighting/Test2.agda | 12 -
examples/syntax/highlighting/Test3.lagda | 98 -
examples/tactics/ac/.cvsignore | 4 -
examples/tactics/ac/AC.agda | 261 -
examples/tactics/ac/Bool.agda | 63 -
examples/tactics/ac/EqProof.agda | 22 -
examples/tactics/ac/Fin.agda | 63 -
examples/tactics/ac/List.agda | 44 -
examples/tactics/ac/Logic.agda | 8 -
examples/tactics/ac/Nat.agda | 29 -
examples/tactics/ac/Vec.agda | 43 -
examples/vfl/Typechecker.agda | 137 -
install-sh | 251 -
macros/.cvsignore | 2 -
macros/fptools.m4 | 29 -
macros/haskell.m4 | 28 -
macros/utils.m4 | 116 -
mk/.cvsignore | 3 -
mk/config.mk.in | 55 -
mk/paths.mk | 19 -
mk/rules.mk | 18 -
notes/.cvsignore | 1 -
notes/builtin | 125 -
notes/classes | 204 -
notes/design/.cvsignore | 1 -
notes/design/fixities | 159 -
notes/design/meeting_050901 | 50 -
notes/design/meeting_050902 | 35 -
notes/design/meeting_050905 | 103 -
notes/design/meeting_050906 | 159 -
notes/design/meeting_050907 | 256 -
notes/design/mutual | 32 -
notes/design/report | 204 -
notes/fixity-declarations | 387 --
notes/inductive-families | 197 -
notes/kit | 20 -
notes/mixfix | 14 -
notes/named-implicit | 52 -
notes/papers/.cvsignore | 2 -
notes/papers/iird/.cvsignore | 1 -
notes/papers/iird/Makefile | 33 -
notes/papers/iird/iird.bib | 10 -
notes/papers/iird/lhs2TeX.fmt | 372 --
notes/papers/iird/lhs2TeX.sty | 120 -
notes/papers/iird/llncs.cls | 1190 ----
notes/papers/iird/macros.tex | 31 -
notes/papers/iird/paper.lhs | 1094 ----
notes/papers/iird/poly.fmt | 380 --
notes/papers/iird/polycode.fmt | 182 -
notes/papers/implicit/.cvsignore | 5 -
notes/papers/implicit/Makefile | 33 -
notes/papers/implicit/abstract.tex | 20 -
notes/papers/implicit/acknowledgement.tex | 9 -
notes/papers/implicit/concl.tex | 22 -
notes/papers/implicit/conclusions.tex | 0
notes/papers/implicit/core.tex | 119 -
notes/papers/implicit/examples.lhs | 133 -
notes/papers/implicit/examples/.cvsignore | 2 -
notes/papers/implicit/examples/Crash.agda | 22 -
notes/papers/implicit/examples/Crash.epi | 42 -
.../papers/implicit/examples/Dangerous-Agda1.agda | 34 -
.../papers/implicit/examples/Dangerous-Agda2.agda | 42 -
.../implicit/examples/Dangerous-AgdaLight.agda | 39 -
notes/papers/implicit/examples/Example.agda | 41 -
notes/papers/implicit/examples/IllTyped.agda | 27 -
notes/papers/implicit/examples/Loop.agda | 37 -
notes/papers/implicit/examples/Scope.agda | 24 -
notes/papers/implicit/examples/Simple.agda | 12 -
notes/papers/implicit/exintro.lhs | 50 -
notes/papers/implicit/implicit.tex | 61 -
notes/papers/implicit/introduction.tex | 83 -
notes/papers/implicit/lhs2TeXpreamble.lhs | 3 -
notes/papers/implicit/llncs.cls | 1190 ----
notes/papers/implicit/macros.tex | 146 -
notes/papers/implicit/notes | 139 -
notes/papers/implicit/proof.sty | 278 -
notes/papers/implicit/proof.tex | 497 --
notes/papers/implicit/rebuttal | 61 -
notes/papers/implicit/relatedwork.tex | 0
notes/papers/implicit/rules.tex | 546 --
notes/papers/modules/notes | 25 -
notes/records | 64 -
notes/releases | 86 -
notes/review/patrik/log.txt | 26 -
notes/scope | 169 -
notes/separate-typechecking | 88 -
notes/talks/.cvsignore | 1 -
notes/talks/MetaVars/.cvsignore | 3 -
notes/talks/MetaVars/Crash.agda | 22 -
notes/talks/MetaVars/Examples.agda | 33 -
notes/talks/MetaVars/Makefile | 5 -
notes/talks/MetaVars/Plus.agda | 25 -
notes/talks/MetaVars/danger_do_not_open_until.eps | 6912 --------------------
notes/talks/MetaVars/danger_do_not_open_until.jpg | Bin 59209 -> 0 bytes
notes/talks/MetaVars/proof.sty | 278 -
notes/talks/MetaVars/talk.tex | 275 -
notes/talks/Modules/.cvsignore | 4 -
notes/talks/Modules/Makefile | 16 -
notes/talks/Modules/notes | 106 -
notes/talks/Modules/proof.sty | 278 -
notes/talks/Modules/talk.tex | 553 --
notes/talks/Types07/.cvsignore | 3 -
notes/talks/Types07/Bad.agda | 25 -
notes/talks/Types07/Makefile | 5 -
notes/talks/Types07/proof.sty | 278 -
notes/talks/Types07/talk.tex | 348 -
notes/talks/video060320/core.tex | 381 --
notes/talks/video060510/.cvsignore | 1 -
notes/talks/video060510/Makefile | 5 -
notes/talks/video060510/abstract | 20 -
notes/talks/video060510/proof.sty | 278 -
notes/talks/video060510/remarks | 135 -
notes/talks/video060510/talk.tex | 539 --
notes/thinkingAloud | 377 --
notes/typechecking/.cvsignore | 2 -
notes/typechecking/Makefile | 13 -
notes/typechecking/agda.tex | 381 --
notes/typechecking/algorithm.tex | 409 --
notes/typechecking/algorithmJ.tex | 332 -
notes/typechecking/core.tex | 936 ---
notes/typechecking/definition | 180 -
notes/typechecking/proof.sty | 278 -
notes/with | 24 -
src/agda-mode/Main.hs | 4 +-
src/compat/Control/Applicative.hs | 222 -
src/compat/Control/Monad/Instances.hs | 24 -
src/compat/Data/ByteString/Lazy.hs | 19 -
src/compat/Data/Foldable.hs | 312 -
src/compat/Data/Monoid/New.hs | 58 -
src/compat/Data/Traversable.hs | 147 -
src/compat/README | 11 -
src/core/.cvsignore | 2 -
src/core/Check.hs | 50 -
src/core/Check.lhs | 138 -
src/core/Cont.hs | 33 -
src/core/Cont.lhs | 66 -
src/core/Conv.hs | 41 -
src/core/Conv.lhs | 132 -
src/core/Core.cf | 63 -
src/core/Decl.hs | 34 -
src/core/Decl.lhs | 76 -
src/core/Exp.hs | 45 -
src/core/Exp.lhs | 86 -
src/core/Main.hs | 17 -
src/core/Makefile | 94 -
src/core/README | 51 -
src/core/Thierry/Check.hs | 54 -
src/core/Thierry/Cont.hs | 31 -
src/core/Thierry/Conv.hs | 54 -
src/core/Thierry/Core.cf | 58 -
src/core/Thierry/Decl1.hs | 107 -
src/core/Thierry/Exp1.hs | 48 -
src/core/Thierry/Main.hs | 34 -
src/core/Thierry/Makefile | 97 -
src/core/Thierry/Val.hs | 55 -
src/core/Thierry/test | 34 -
src/core/Thierry/test1 | 3 -
src/core/Thierry/test2 | 9 -
src/core/Thierry/test3 | 9 -
src/core/Thierry/test4 | 4 -
src/core/Thierry/test5 | 33 -
src/core/Val.hs | 49 -
src/core/Val.lhs | 92 -
src/core/instructions-for-lhs | 6 -
src/core/main.lhs | 23 -
src/core/overview.tex | 52 -
src/data/agda.sty | 329 +-
src/data/emacs-mode/agda-input.el | 349 +-
src/data/emacs-mode/agda2-highlight.el | 43 +-
src/data/emacs-mode/agda2-mode.el | 198 +-
src/data/lib/prim/Agda/Primitive.agda | 34 +
src/fix-agda-whitespace/FixWhitespace.hs | 104 -
src/fix-agda-whitespace/fix-agda-whitespace.cabal | 12 -
src/full/.cvsignore | 2 -
src/full/Agda/Auto/Auto.hs | 77 +-
src/full/Agda/Auto/CaseSplit.hs | 21 +-
src/full/Agda/Auto/Convert.hs | 245 +-
src/full/Agda/Auto/NarrowingSearch.hs | 69 +-
src/full/Agda/Auto/SearchControl.hs | 12 +-
src/full/Agda/Auto/Syntax.hs | 219 +-
src/full/Agda/Auto/Typecheck.hs | 18 +-
src/full/Agda/Compiler/CallCompiler.hs | 2 +-
src/full/Agda/Compiler/Epic/AuxAST.hs | 1 +
src/full/Agda/Compiler/Epic/CaseOpts.hs | 2 -
src/full/Agda/Compiler/Epic/CompileState.hs | 5 +-
src/full/Agda/Compiler/Epic/Compiler.hs | 16 +-
src/full/Agda/Compiler/Epic/Epic.hs | 14 +-
src/full/Agda/Compiler/Epic/Erasure.hs | 7 +-
src/full/Agda/Compiler/Epic/ForceConstrs.hs | 9 +-
src/full/Agda/Compiler/Epic/Forcing.hs | 59 +-
src/full/Agda/Compiler/Epic/FromAgda.hs | 38 +-
src/full/Agda/Compiler/Epic/Injection.hs | 217 +-
src/full/Agda/Compiler/Epic/Interface.hs | 2 -
src/full/Agda/Compiler/Epic/NatDetection.hs | 6 +-
src/full/Agda/Compiler/Epic/Primitive.hs | 2 +-
src/full/Agda/Compiler/Epic/Smashing.hs | 19 +-
src/full/Agda/Compiler/Epic/Static.hs | 79 +-
src/full/Agda/Compiler/HaskellTypes.hs | 37 +-
src/full/Agda/Compiler/JS/Case.hs | 4 +-
src/full/Agda/Compiler/JS/Compiler.hs | 186 +-
src/full/Agda/Compiler/JS/Parser.hs | 8 +-
src/full/Agda/Compiler/JS/Substitution.hs | 6 +-
src/full/Agda/Compiler/MAlonzo/Compiler.hs | 131 +-
src/full/Agda/Compiler/MAlonzo/Misc.hs | 47 +-
src/full/Agda/Compiler/MAlonzo/Pretty.hs | 6 +-
src/full/Agda/Compiler/MAlonzo/Primitives.hs | 29 +-
src/full/Agda/ImpossibleTest.hs | 4 +-
src/full/Agda/Interaction/.cvsignore | 2 -
src/full/Agda/Interaction/BasicOps.hs | 539 +-
src/full/Agda/Interaction/CommandLine/.cvsignore | 2 -
.../Agda/Interaction/CommandLine/CommandLine.hs | 19 +-
.../Agda/Interaction/{GhcTop.hs => EmacsTop.hs} | 86 +-
src/full/Agda/Interaction/Exceptions.hs | 2 -
src/full/Agda/Interaction/FindFile.hs | 47 +-
src/full/Agda/Interaction/Highlighting/.cvsignore | 2 -
src/full/Agda/Interaction/Highlighting/Dot.hs | 54 +-
src/full/Agda/Interaction/Highlighting/Emacs.hs | 14 +-
src/full/Agda/Interaction/Highlighting/Generate.hs | 154 +-
src/full/Agda/Interaction/Highlighting/HTML.hs | 41 +-
src/full/Agda/Interaction/Highlighting/LaTeX.hs | 291 +-
src/full/Agda/Interaction/Highlighting/Precise.hs | 19 +-
src/full/Agda/Interaction/Highlighting/Vim.hs | 25 +-
src/full/Agda/Interaction/Imports.hs | 400 +-
src/full/Agda/Interaction/InteractionTop.hs | 782 ++-
src/full/Agda/Interaction/MakeCase.hs | 104 +-
src/full/Agda/Interaction/Options.hs | 93 +-
src/full/Agda/Interaction/Options/Lenses.hs | 189 +
src/full/Agda/Interaction/Response.hs | 44 +-
src/full/Agda/Interaction/Response.hs-boot | 1 +
src/full/Agda/Main.hs | 114 +-
src/full/Agda/Packaging/Config.hs | 23 -
src/full/Agda/Packaging/Database.hs | 234 -
src/full/Agda/Packaging/Monad.hs | 38 -
src/full/Agda/Packaging/Types.hs | 20 -
src/full/Agda/Syntax/.cvsignore | 1 -
src/full/Agda/Syntax/Abstract.hs | 417 +-
src/full/Agda/Syntax/Abstract/.cvsignore | 2 -
src/full/Agda/Syntax/Abstract/Copatterns.hs | 30 +-
src/full/Agda/Syntax/Abstract/Name.hs | 148 +-
src/full/Agda/Syntax/Abstract/Pretty.hs | 6 +-
src/full/Agda/Syntax/Abstract/Views.hs | 131 +-
src/full/Agda/Syntax/Common.hs | 469 +-
src/full/Agda/Syntax/Concrete.hs | 221 +-
src/full/Agda/Syntax/Concrete/.cvsignore | 1 -
src/full/Agda/Syntax/Concrete/Definitions.hs | 280 +-
src/full/Agda/Syntax/Concrete/Generic.hs | 190 +
src/full/Agda/Syntax/Concrete/Name.hs | 219 +-
src/full/Agda/Syntax/Concrete/Operators.hs | 148 +-
src/full/Agda/Syntax/Concrete/Operators/Parser.hs | 118 +-
src/full/Agda/Syntax/Concrete/Pretty.hs | 158 +-
src/full/Agda/Syntax/Fixity.hs | 10 +-
src/full/Agda/Syntax/Info.hs | 44 +-
src/full/Agda/Syntax/Internal.hs | 460 +-
src/full/Agda/Syntax/Internal/Defs.hs | 119 +
src/full/Agda/Syntax/Internal/Generic.hs | 55 +-
src/full/Agda/Syntax/Internal/Pattern.hs | 140 +-
src/full/Agda/Syntax/Notation.hs | 67 +-
src/full/Agda/Syntax/Parser.hs | 7 +-
src/full/Agda/Syntax/Parser/.cvsignore | 1 -
src/full/Agda/Syntax/Parser/Comments.hs | 5 +-
src/full/Agda/Syntax/Parser/Layout.hs | 2 +-
src/full/Agda/Syntax/Parser/LexActions.hs | 6 +-
src/full/Agda/Syntax/Parser/Lexer.x | 18 +-
src/full/Agda/Syntax/Parser/LookAhead.hs | 5 +-
src/full/Agda/Syntax/Parser/Monad.hs | 8 +-
src/full/Agda/Syntax/Parser/Parser.y | 412 +-
src/full/Agda/Syntax/Parser/StringLiterals.hs | 1 -
src/full/Agda/Syntax/Parser/Tokens.hs | 8 +-
src/full/Agda/Syntax/Position.hs | 188 +-
src/full/Agda/Syntax/Scope/Base.hs | 310 +-
src/full/Agda/Syntax/Scope/Monad.hs | 103 +-
src/full/Agda/Syntax/Translation/.cvsignore | 1 -
.../Agda/Syntax/Translation/AbstractToConcrete.hs | 320 +-
.../Agda/Syntax/Translation/ConcreteToAbstract.hs | 604 +-
.../Agda/Syntax/Translation/InternalToAbstract.hs | 664 +-
src/full/Agda/Termination/CallGraph.hs | 748 +--
src/full/Agda/Termination/CallMatrix.hs | 318 +
src/full/Agda/Termination/CutOff.hs | 19 +
src/full/Agda/Termination/FoetusTermination.hs | 256 -
src/full/Agda/Termination/Inlining.hs | 241 +
src/full/Agda/Termination/Lexicographic.hs | 243 -
src/full/Agda/Termination/Matrix.hs | 340 -
src/full/Agda/Termination/Monad.hs | 451 ++
src/full/Agda/Termination/Order.hs | 369 ++
src/full/Agda/Termination/RecCheck.hs | 64 +
src/full/Agda/Termination/Semiring.hs | 19 +-
src/full/Agda/Termination/SparseMatrix.hs | 797 ++-
src/full/Agda/Termination/TermCheck.hs | 1697 +++--
src/full/Agda/Termination/Termination.hs | 224 +-
src/full/Agda/Tests.hs | 30 +-
src/full/Agda/TheTypeChecker.hs | 8 +
src/full/Agda/TypeChecker.hs | 13 -
src/full/Agda/TypeChecking/.cvsignore | 1 -
src/full/Agda/TypeChecking/Abstract.hs | 79 +-
src/full/Agda/TypeChecking/CheckInternal.hs | 322 +
src/full/Agda/TypeChecking/CheckInternal.hs-boot | 7 +
src/full/Agda/TypeChecking/CompiledClause.hs | 48 +-
.../Agda/TypeChecking/CompiledClause/Compile.hs | 109 +-
src/full/Agda/TypeChecking/CompiledClause/Match.hs | 258 +-
.../Agda/TypeChecking/CompiledClause/Match.hs-boot | 6 +-
src/full/Agda/TypeChecking/Constraints.hs | 39 +-
src/full/Agda/TypeChecking/Conversion.hs | 798 ++-
src/full/Agda/TypeChecking/Conversion.hs-boot | 1 +
src/full/Agda/TypeChecking/Coverage.hs | 404 +-
src/full/Agda/TypeChecking/Coverage/Match.hs | 119 +-
src/full/Agda/TypeChecking/Coverage/SplitTree.hs | 4 +-
src/full/Agda/TypeChecking/Datatypes.hs | 67 +-
src/full/Agda/TypeChecking/Datatypes.hs-boot | 4 +-
src/full/Agda/TypeChecking/DisplayForm.hs | 141 +-
src/full/Agda/TypeChecking/DropArgs.hs | 15 +-
src/full/Agda/TypeChecking/Eliminators.hs | 82 -
src/full/Agda/TypeChecking/Empty.hs | 10 +-
src/full/Agda/TypeChecking/Errors.hs | 347 +-
src/full/Agda/TypeChecking/Errors.hs-boot | 4 +-
src/full/Agda/TypeChecking/EtaContract.hs | 85 +-
src/full/Agda/TypeChecking/Forcing.hs | 12 +-
src/full/Agda/TypeChecking/Free.hs | 27 +-
src/full/Agda/TypeChecking/Implicit.hs | 56 +-
src/full/Agda/TypeChecking/Injectivity.hs | 141 +-
src/full/Agda/TypeChecking/InstanceArguments.hs | 153 +-
src/full/Agda/TypeChecking/Irrelevance.hs | 24 +-
src/full/Agda/TypeChecking/Level.hs | 46 +-
src/full/Agda/TypeChecking/LevelConstraints.hs | 4 +-
src/full/Agda/TypeChecking/MetaVars.hs | 644 +-
src/full/Agda/TypeChecking/MetaVars.hs-boot | 10 +-
src/full/Agda/TypeChecking/MetaVars/Mention.hs | 15 +-
src/full/Agda/TypeChecking/MetaVars/Occurs.hs | 241 +-
src/full/Agda/TypeChecking/Monad/.cvsignore | 1 -
src/full/Agda/TypeChecking/Monad/Base.hs | 824 ++-
src/full/Agda/TypeChecking/Monad/Base.hs-boot | 6 +-
src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs | 75 +
src/full/Agda/TypeChecking/Monad/Base/KillRange.hs | 114 +
src/full/Agda/TypeChecking/Monad/Benchmark.hs | 81 +
src/full/Agda/TypeChecking/Monad/Builtin.hs | 95 +-
src/full/Agda/TypeChecking/Monad/Closure.hs | 2 -
src/full/Agda/TypeChecking/Monad/Constraints.hs | 8 +-
src/full/Agda/TypeChecking/Monad/Context.hs | 152 +-
src/full/Agda/TypeChecking/Monad/Context.hs-boot | 1 -
src/full/Agda/TypeChecking/Monad/Env.hs | 47 +-
src/full/Agda/TypeChecking/Monad/Imports.hs | 12 +-
src/full/Agda/TypeChecking/Monad/MetaVars.hs | 286 +-
src/full/Agda/TypeChecking/Monad/Mutual.hs | 6 +-
src/full/Agda/TypeChecking/Monad/Open.hs | 11 +-
src/full/Agda/TypeChecking/Monad/Options.hs | 195 +-
src/full/Agda/TypeChecking/Monad/Options.hs-boot | 20 +
src/full/Agda/TypeChecking/Monad/Sharing.hs | 4 +-
src/full/Agda/TypeChecking/Monad/Signature.hs | 417 +-
src/full/Agda/TypeChecking/Monad/SizedTypes.hs | 69 +-
src/full/Agda/TypeChecking/Monad/State.hs | 195 +-
src/full/Agda/TypeChecking/Monad/Statistics.hs | 42 +-
src/full/Agda/TypeChecking/Monad/Trace.hs | 23 +-
src/full/Agda/TypeChecking/Patterns/.cvsignore | 1 -
src/full/Agda/TypeChecking/Patterns/Abstract.hs | 123 +
src/full/Agda/TypeChecking/Patterns/Match.hs | 194 +-
src/full/Agda/TypeChecking/Patterns/Match.hs-boot | 7 +-
src/full/Agda/TypeChecking/Polarity.hs | 97 +-
src/full/Agda/TypeChecking/Positivity.hs | 91 +-
src/full/Agda/TypeChecking/Pretty.hs | 91 +-
src/full/Agda/TypeChecking/Pretty.hs-boot | 8 +-
src/full/Agda/TypeChecking/Primitive.hs | 220 +-
src/full/Agda/TypeChecking/ProjectionLike.hs | 213 +-
src/full/Agda/TypeChecking/ProjectionLike.hs-boot | 2 +-
src/full/Agda/TypeChecking/Quote.hs | 110 +-
src/full/Agda/TypeChecking/Rebind.hs | 17 -
src/full/Agda/TypeChecking/RecordPatterns.hs | 103 +-
src/full/Agda/TypeChecking/Records.hs | 347 +-
src/full/Agda/TypeChecking/Records.hs-boot | 9 +-
src/full/Agda/TypeChecking/Reduce.hs | 1215 ++--
src/full/Agda/TypeChecking/Reduce/Monad.hs | 185 +
src/full/Agda/TypeChecking/Rules/Builtin.hs | 106 +-
.../Agda/TypeChecking/Rules/Builtin/Coinduction.hs | 89 +-
src/full/Agda/TypeChecking/Rules/Data.hs | 260 +-
src/full/Agda/TypeChecking/Rules/Decl.hs | 503 +-
src/full/Agda/TypeChecking/Rules/Decl.hs-boot | 2 +-
src/full/Agda/TypeChecking/Rules/Def.hs | 559 +-
src/full/Agda/TypeChecking/Rules/Def.hs-boot | 3 +-
src/full/Agda/TypeChecking/Rules/LHS.hs | 254 +-
src/full/Agda/TypeChecking/Rules/LHS/Implicit.hs | 124 +-
.../Agda/TypeChecking/Rules/LHS/Instantiate.hs | 58 +-
src/full/Agda/TypeChecking/Rules/LHS/Problem.hs | 144 +-
.../Agda/TypeChecking/Rules/LHS/ProblemRest.hs | 124 +-
src/full/Agda/TypeChecking/Rules/LHS/Split.hs | 312 +-
src/full/Agda/TypeChecking/Rules/LHS/Unify.hs | 410 +-
src/full/Agda/TypeChecking/Rules/Record.hs | 229 +-
src/full/Agda/TypeChecking/Rules/Term.hs | 1333 ++--
src/full/Agda/TypeChecking/Rules/Term.hs-boot | 6 +-
src/full/Agda/TypeChecking/Serialise.hs | 384 +-
src/full/Agda/TypeChecking/SizedTypes.hs | 452 +-
src/full/Agda/TypeChecking/SizedTypes/Solve.hs | 451 ++
src/full/Agda/TypeChecking/SizedTypes/Syntax.hs | 279 +
src/full/Agda/TypeChecking/SizedTypes/Tests.hs | 119 +
src/full/Agda/TypeChecking/SizedTypes/Utils.hs | 31 +
.../Agda/TypeChecking/SizedTypes/WarshallSolver.hs | 922 +++
src/full/Agda/TypeChecking/Substitute.hs | 515 +-
src/full/Agda/TypeChecking/SyntacticEquality.hs | 200 +
src/full/Agda/TypeChecking/Telescope.hs | 15 +-
src/full/Agda/TypeChecking/Test/Generators.hs | 157 +-
src/full/Agda/TypeChecking/UniversePolymorphism.hs | 28 -
.../Agda/TypeChecking/UniversePolymorphism.hs-boot | 7 -
src/full/Agda/TypeChecking/With.hs | 259 +-
src/full/Agda/Utils/.cvsignore | 2 -
src/full/Agda/Utils/BiMap.hs | 106 +
src/full/Agda/Utils/Cluster.hs | 93 +
src/full/Agda/Utils/Either.hs | 51 +-
src/full/Agda/Utils/Favorites.hs | 195 +
src/full/Agda/Utils/FileName.hs | 40 +-
src/full/Agda/Utils/Function.hs | 55 +
src/full/Agda/Utils/Functor.hs | 77 +
.../Agda/Utils/{Graph.hs => Graph/AdjacencyMap.hs} | 139 +-
.../Utils/Graph/AdjacencyMap/Unidirectional.hs | 552 ++
src/full/Agda/Utils/Hash.hs | 30 +-
src/full/Agda/Utils/List.hs | 113 +-
src/full/Agda/Utils/Map.hs | 11 +-
src/full/Agda/Utils/Maybe.hs | 75 +-
src/full/Agda/Utils/Maybe/Strict.hs | 196 +
src/full/Agda/Utils/Monad.hs | 74 +-
src/full/Agda/Utils/Monad/.cvsignore | 2 -
src/full/Agda/Utils/NubList.hs | 49 -
src/full/Agda/Utils/Null.hs | 43 +
src/full/Agda/Utils/PartialOrd.hs | 429 ++
src/full/Agda/Utils/Permutation.hs | 71 +-
src/full/Agda/Utils/Pointed.hs | 5 +
src/full/Agda/Utils/Pointer.hs | 2 -
src/full/Agda/Utils/Pretty.hs | 6 +-
src/full/Agda/Utils/QuickCheck.hs | 6 +-
src/full/Agda/Utils/ReadP.hs | 20 +-
src/full/Agda/Utils/String.hs | 7 +
src/full/Agda/Utils/Suffix.hs | 4 +-
src/full/Agda/Utils/TestHelpers.hs | 33 +-
src/full/Agda/Utils/Trie.hs | 94 +-
src/full/Agda/Utils/Tuple.hs | 11 +-
src/full/Agda/Utils/Update.hs | 92 +-
src/full/Agda/Utils/VarSet.hs | 2 +-
src/full/Agda/Utils/Warshall.hs | 136 +-
src/full/Makefile | 125 -
src/hTags/Main.hs | 180 -
src/hTags/Makefile | 15 -
src/hTags/Setup.hs | 4 -
src/hTags/Tags.hs | 284 -
src/hTags/hTags.cabal | 20 -
src/main/.cvsignore | 1 -
src/main/Makefile | 34 -
src/main/Setup.hs | 4 -
src/pkg/Interface/Command.hs | 15 -
src/pkg/Interface/Command/Describe.hs | 0
src/pkg/Interface/Command/Dump.hs | 29 -
src/pkg/Interface/Command/Field.hs | 0
src/pkg/Interface/Command/List.hs | 86 -
src/pkg/Interface/Command/Register.hs | 80 -
src/pkg/Interface/Command/Unregister.hs | 12 -
src/pkg/Interface/Command/Visibility.hs | 37 -
src/pkg/Interface/Exit.hs | 43 -
src/pkg/Interface/Options.hs | 33 -
src/pkg/Interface/Usage.hs | 53 -
src/pkg/Interface/Version.hs | 10 -
src/pkg/Main.hs | 133 -
src/pkg/TODO | 1 -
src/pkg/Utils.hs | 36 -
src/prototyping/eval/.cvsignore | 3 -
src/prototyping/eval/Data/Trie.hs | 85 -
src/prototyping/eval/DeBruijnCBN.hs | 111 -
src/prototyping/eval/DeBruijnCBN2.hs | 125 -
src/prototyping/eval/DeBruijnCBN3.hs | 119 -
src/prototyping/eval/DeBruijnCBN4.hs | 165 -
src/prototyping/eval/DeBruijnCBN5.hs | 170 -
src/prototyping/eval/DeBruijnCBN6.hs | 175 -
src/prototyping/eval/DeBruijnCBN7.hs | 222 -
src/prototyping/eval/DeBruijnLazy1.hs | 270 -
src/prototyping/eval/DeBruijnLazy2.hs | 271 -
src/prototyping/eval/DeBruijnLazy3.hs | 273 -
src/prototyping/eval/DeBruijnLazy4.hs | 301 -
src/prototyping/eval/DeBruijnLazy5.hs | 309 -
src/prototyping/eval/DeBruijnLazy6.hs | 311 -
src/prototyping/eval/DeBruijnLazy7.hs | 305 -
src/prototyping/eval/Lam.cf | 34 -
src/prototyping/eval/Main.hs | 75 -
src/prototyping/eval/Makefile | 39 -
src/prototyping/eval/Parse.hs | 142 -
src/prototyping/eval/Pointer.hs | 49 -
src/prototyping/eval/PointerST.hs | 33 -
src/prototyping/eval/Pretty.hs | 75 -
src/prototyping/eval/Syntax.hs | 41 -
src/prototyping/eval/Utils.hs | 6 -
src/prototyping/eval/church.lam | 74 -
src/prototyping/eval/nat.lam | 73 -
src/prototyping/eval/notes | 18 -
src/prototyping/mixfix/.cvsignore | 1 -
src/prototyping/mixfix/Expression.hs | 66 -
src/prototyping/mixfix/ExpressionParser.hs | 235 -
src/prototyping/mixfix/IndexedMap.hs | 79 -
src/prototyping/mixfix/IndexedOrd.hs | 71 -
src/prototyping/mixfix/Memoised.hs | 113 -
src/prototyping/mixfix/MemoisedCPS.hs | 141 -
src/prototyping/mixfix/Name.hs | 162 -
src/prototyping/mixfix/Parser.hs | 63 -
src/prototyping/mixfix/PrecedenceGraph.hs | 366 --
src/prototyping/mixfix/Test.hs | 342 -
src/prototyping/mixfix/Token.hs | 298 -
src/prototyping/mixfix/Utilities.hs | 304 -
src/prototyping/mixfix/benchmarks/AmbExTrie.hs | 64 -
src/prototyping/mixfix/benchmarks/AmbExTrie2.hs | 86 -
src/prototyping/mixfix/benchmarks/AmbTrie.hs | 50 -
src/prototyping/mixfix/benchmarks/ContTrans.hs | 39 -
src/prototyping/mixfix/benchmarks/Incremental.hs | 27 -
src/prototyping/mixfix/benchmarks/Memoised.hs | 80 -
src/prototyping/mixfix/benchmarks/MemoisedCPS.hs | 129 -
src/prototyping/mixfix/benchmarks/Parser.hs | 51 -
.../mixfix/benchmarks/PrecedenceGraph.hs | 322 -
src/prototyping/mixfix/benchmarks/ReadP.hs | 477 --
src/prototyping/mixfix/benchmarks/ReadPWrapper.hs | 35 -
src/prototyping/mixfix/benchmarks/SlowParser.hs | 50 -
.../mixfix/benchmarks/StackContTrans.hs | 35 -
src/prototyping/mixfix/benchmarks/Standard.hs | 37 -
src/prototyping/mixfix/benchmarks/Test.hs | 245 -
.../mixfix/benchmarks/mixfix-benchmarks.cabal | 16 -
src/prototyping/mixfix/old/Makefile | 15 -
src/prototyping/mixfix/old/MixFix.hs | 296 -
src/prototyping/mixfix/old/MixFix2.hs | 297 -
src/prototyping/mixfix/old/ReadP.hs | 477 --
src/prototyping/modules/Modules.hs | 553 --
src/prototyping/modules/ModulesAttempt1.hs | 159 -
src/prototyping/modules/ModulesAttempt2.hs | 354 -
src/prototyping/modules/flat/.cvsignore | 1 -
src/prototyping/modules/flat/Abstract.hs | 88 -
src/prototyping/modules/flat/Debug.hs | 8 -
src/prototyping/modules/flat/Internal.hs | 63 -
src/prototyping/modules/flat/Main.hs | 58 -
src/prototyping/modules/flat/Makefile | 20 -
src/prototyping/modules/flat/Pretty.hs | 14 -
src/prototyping/modules/flat/Scope.hs | 458 --
src/prototyping/modules/flat/Syntax.cf | 60 -
src/prototyping/modules/flat/Test.agda | 22 -
src/prototyping/modules/flat/TypeCheck.hs | 259 -
src/prototyping/modules/flat/Utils.hs | 10 -
src/prototyping/modules/flat/test.mod | 126 -
src/prototyping/nameless/Lam.cf | 31 -
src/prototyping/nameless/Main.hs | 40 -
src/prototyping/nameless/Makefile | 22 -
src/prototyping/nameless/Name.hs | 17 -
src/prototyping/nameless/Stack.hs | 28 -
src/prototyping/nameless/Syntax.hs | 104 -
src/prototyping/nameless/TypeChecker.hs | 223 -
src/prototyping/nameless/test.lam | 36 -
src/prototyping/subst/Subst.agda | 129 -
src/prototyping/termrep/Main.hs | 64 -
src/prototyping/termrep/Makefile | 16 -
src/prototyping/termrep/Syntax.cf | 31 -
src/prototyping/termrep/Syntax/Abstract.hs | 39 -
src/prototyping/termrep/Syntax/Desugar.hs | 196 -
src/prototyping/termrep/Syntax/Pretty.hs | 49 -
src/prototyping/termrep/Terms/Interface.hs | 4 -
src/prototyping/termrep/Terms/None.hs | 37 -
src/prototyping/termrep/Types/Check.hs | 68 -
src/prototyping/termrep/Types/Equality.hs | 8 -
src/prototyping/termrep/Types/Metas.hs | 8 -
src/prototyping/termrep/Types/Monad.hs | 77 -
src/prototyping/termrep/happy.out | 876 ---
src/prototyping/termrep/lambdapi/LambdaPi.hs | 1072 ---
src/prototyping/termrep/lambdapi/cat.lp | 1 -
src/prototyping/termrep/lambdapi/prelude.lp | 319 -
src/prototyping/termrep/test.pi | 45 -
src/prototyping/terms/Check.hs | 33 -
src/prototyping/terms/Eval.hs | 52 -
src/prototyping/terms/Main.hs | 32 -
src/prototyping/terms/Makefile | 21 -
src/prototyping/terms/Monad.hs | 86 -
src/prototyping/terms/Name.hs | 10 -
src/prototyping/terms/Pretty.hs | 14 -
src/prototyping/terms/Syntax.cf | 14 -
src/prototyping/terms/Term.hs | 43 -
src/prototyping/terms/example.lam | 15 -
src/prototyping/trace/.cvsignore | 1 -
src/prototyping/trace/Lambda.cf | 10 -
src/prototyping/trace/Main.hs | 24 -
src/prototyping/trace/Makefile | 66 -
src/prototyping/trace/TypeChecker.hs | 232 -
src/prototyping/trace/tests.lam | 7 -
src/rts/Makefile | 10 -
src/rts/RTN.agda | 9 -
src/rts/RTN.hs | 13 -
src/rts/RTP.agda | 42 -
src/rts/RTP.hs | 116 -
src/rts/RTS.hs | 9 -
src/rts/Setup.hs | 4 -
src/rts/agda-rts.cabal | 13 -
src/transl/.cvsignore | 2 -
src/transl/INSTALL | 17 -
src/transl/Main.hs | 71 -
src/transl/README | 89 -
src/transl/Setup.hs | 2 -
src/transl/Translator.hs | 692 --
src/transl/agda/.cvsignore | 2 -
src/transl/agda/AgdaPretty.hs | 100 -
src/transl/agda/AgdaScans.hs | 37 -
src/transl/agda/AgdaTrace.hs | 4 -
src/transl/agda/AltIntMap.hs | 26 -
src/transl/agda/BinParse.hs | 42 -
src/transl/agda/CITrans.hs | 112 -
src/transl/agda/CParser.hs | 566 --
src/transl/agda/CPrinter.hs | 522 --
src/transl/agda/CSyntax.hs | 475 --
src/transl/agda/Error.hs | 317 -
src/transl/agda/FString.hs | 126 -
src/transl/agda/Hash.hs | 117 -
src/transl/agda/ISynEnv.hs | 154 -
src/transl/agda/ISynType.hs | 528 --
src/transl/agda/ISyntax.hs | 474 --
src/transl/agda/Id.hs | 265 -
src/transl/agda/Lex.hs | 399 --
src/transl/agda/Literal.hs | 26 -
src/transl/agda/MetaVars.hs | 24 -
src/transl/agda/MiscId.hs | 67 -
src/transl/agda/Monads.hs | 137 -
src/transl/agda/NewCParser.hs | 7 -
src/transl/agda/OldCParser.hs | 7 -
src/transl/agda/PPrint.hs | 97 -
src/transl/agda/Parse.hs | 260 -
src/transl/agda/PluginType.hs | 32 -
src/transl/agda/Position.hs | 50 -
src/transl/agda/PreStrings.hs | 50 -
src/transl/agda/Util.hs | 165 -
src/transl/agda/Utilities.hs | 149 -
src/transl/agda/config.h | 5 -
src/transl/agda1to2.cabal | 21 -
test/.cvsignore | 1 -
test/Common/Char.agda | 7 -
test/Common/Coinduction.agda | 19 -
test/Common/Equality.agda | 17 -
test/Common/FFI.hs | 11 -
test/Common/Irrelevance.agda | 14 -
test/Common/Issue481ParametrizedModule.agda | 7 -
test/Common/Level.agda | 32 -
test/Common/MAlonzo.agda | 23 -
test/Common/Prelude.agda | 75 -
test/Common/Product.agda | 28 -
test/Common/Reflect.agda | 106 -
test/Common/Size.agda | 16 -
test/bugs/.cvsignore | 2 -
test/bugs/FamilyPattern.agda | 14 -
test/bugs/ImpossiblePattern.agda | 6 -
test/bugs/Issue166NotSized.agda | 22 -
test/bugs/Issue325b.agda | 44 -
test/bugs/Lambda.agda | 18 -
test/bugs/Mutual.agda | 45 -
test/bugs/RecursiveRecord.agda | 16 -
test/bugs/SizedTypesLoopDueInadmissibility.agda | 56 -
test/bugs/SizedTypesMergeSort.agda | 45 -
test/bugs/SizedTypesScopeViolationInMeta.agda | 29 -
test/bugs/TerminationSubpattern.agda | 33 -
test/bugs/fixed/DotPattern.agda | 64 -
test/bugs/fixed/DroppingParameters.agda | 25 -
test/bugs/fixed/HiddenLambda.agda | 14 -
test/bugs/fixed/LostConstraint.agda | 38 -
test/bugs/fixed/lexerBug.agda | 1 -
test/bugs/univ.agda | 324 -
test/compiler/Main.agda | 25 -
test/core/core.agda | 8 -
test/epic/Makefile | 6 -
test/epic/Prelude/Bool.agda | 29 -
test/epic/Prelude/Bot.agda | 6 -
test/epic/Prelude/Char.agda | 22 -
test/epic/Prelude/Eq.agda | 16 -
test/epic/Prelude/FFI.agda | 19 -
test/epic/Prelude/File.agda | 163 -
test/epic/Prelude/File2.agda | 192 -
test/epic/Prelude/Fin.agda | 20 -
test/epic/Prelude/Float.agda | 12 -
test/epic/Prelude/IO.agda | 78 -
test/epic/Prelude/Level.agda | 12 -
test/epic/Prelude/List.agda | 74 -
test/epic/Prelude/Nat.agda | 45 -
test/epic/Prelude/Product.agda | 9 -
test/epic/Prelude/Stream.agda | 76 -
test/epic/Prelude/String.agda | 38 -
test/epic/Prelude/Unit.agda | 6 -
test/epic/Prelude/Vec.agda | 58 -
test/epic/RunTests.agda | 183 -
test/epic/tests/Arith.agda | 24 -
test/epic/tests/Arith.out | 1 -
test/epic/tests/Cat.agda | 250 -
test/epic/tests/Cat.out | 4 -
test/epic/tests/Coind.agda | 42 -
test/epic/tests/Coind.out | 3 -
test/epic/tests/Forcing.agda | 52 -
test/epic/tests/Forcing.out | 1 -
test/epic/tests/Forcing2.agda | 32 -
test/epic/tests/Forcing2.out | 1 -
test/epic/tests/Forcing3.agda | 55 -
test/epic/tests/Forcing3.out | 1 -
test/epic/tests/Forcing4.agda | 65 -
test/epic/tests/Forcing4.out | 2 -
test/epic/tests/Literals.agda | 29 -
test/epic/tests/Literals.out | 1 -
test/epic/tests/Mutual.agda | 41 -
test/epic/tests/Mutual.out | 2 -
test/epic/tests/PrintBool.agda | 37 -
test/epic/tests/PrintBool.out | 3 -
test/epic/tests/String.agda | 24 -
test/epic/tests/String.out | 3 -
test/fail/.cvsignore | 2 -
test/fail/A/B/M.agda | 1 -
test/fail/A/M.agda | 3 -
test/fail/AbsToConDecl.agda | 5 -
test/fail/AbsToConDecl.err | 8 -
test/fail/Abstract.agda | 28 -
test/fail/Abstract.err | 3 -
test/fail/AbstractBlockInLet.agda | 10 -
test/fail/AbstractBlockInLet.err | 8 -
test/fail/AbsurdPatternRequiresNoRHS.agda | 8 -
test/fail/AbsurdPatternRequiresNoRHS.err | 4 -
test/fail/AgdalightTelescopeSyntax.agda | 7 -
test/fail/AgdalightTelescopeSyntax.err | 3 -
test/fail/AmbiguousModule.agda | 9 -
test/fail/AmbiguousModule.err | 5 -
test/fail/AmbiguousName.agda | 14 -
test/fail/AmbiguousName.err | 5 -
test/fail/AmbiguousParseForApplication.agda | 11 -
test/fail/AmbiguousParseForApplication.err | 6 -
test/fail/AmbiguousParseForLHS.agda | 11 -
test/fail/AmbiguousParseForLHS.err | 7 -
test/fail/AmbiguousTopLevelModuleName.agda | 3 -
test/fail/AmbiguousTopLevelModuleName.err | 7 -
test/fail/BadInductionRecursion1.agda | 21 -
test/fail/BadInductionRecursion1.err | 4 -
test/fail/BadInductionRecursion2.agda | 21 -
test/fail/BadInductionRecursion2.err | 4 -
test/fail/BadInductionRecursion3.agda | 27 -
test/fail/BadInductionRecursion3.err | 5 -
test/fail/BadTermination.agda | 16 -
test/fail/BadTermination.err | 6 -
test/fail/BoundedSizeNoMatch.agda | 20 -
test/fail/BoundedSizeNoMatch.err | 6 -
.../BrokenInferenceDueToNonvariantPolarity.agda | 56 -
.../BrokenInferenceDueToNonvariantPolarity.err | 4 -
.../fail/BuiltinConstructorsNeededForLiterals.agda | 17 -
test/fail/BuiltinConstructorsNeededForLiterals.err | 4 -
test/fail/BuiltinInParameterisedModule.agda | 7 -
test/fail/BuiltinInParameterisedModule.err | 4 -
test/fail/BuiltinMustBeConstructor.agda | 12 -
test/fail/BuiltinMustBeConstructor.err | 3 -
.../fail/CantOpenConstructorsFromRecordModule.agda | 14 -
test/fail/CantOpenConstructorsFromRecordModule.err | 5 -
test/fail/CheckSizeMetaBounds.agda | 41 -
test/fail/CheckSizeMetaBounds.err | 5 -
test/fail/ClashingDefinition.agda | 9 -
test/fail/ClashingDefinition.err | 5 -
test/fail/ClashingImport.agda | 9 -
test/fail/ClashingImport.err | 5 -
test/fail/ClashingModule.agda | 7 -
test/fail/ClashingModule.err | 5 -
test/fail/ClashingModuleImport.agda | 3 -
test/fail/ClashingModuleImport.err | 5 -
test/fail/Codata.agda | 3 -
test/fail/Codata.err | 3 -
test/fail/CoinductiveBuiltinList.agda | 0
test/fail/CoinductiveBuiltinList.err | 0
test/fail/CoinductiveBuiltinNatural.agda | 11 -
test/fail/CoinductiveBuiltinNatural.err | 3 -
test/fail/CoinductiveConstructorsAndLet.agda | 13 -
test/fail/CoinductiveConstructorsAndLet.err | 4 -
test/fail/CoinductiveUnitRecord.agda | 26 -
test/fail/CoinductiveUnitRecord.err | 8 -
test/fail/ColistMutual.agda | 53 -
test/fail/ColistMutual.err | 8 -
test/fail/CompiledMustBePostulate.agda | 11 -
test/fail/CompiledMustBePostulate.err | 3 -
test/fail/CompiledMustHaveHaskellType.agda | 12 -
test/fail/CompiledMustHaveHaskellType.err | 3 -
test/fail/ComplexIMPORT.agda | 3 -
test/fail/ComplexIMPORT.err | 3 -
test/fail/ConstructorHeadedDivergenceIn2-2-10.agda | 48 -
test/fail/ConstructorHeadedDivergenceIn2-2-10.err | 4 -
test/fail/CopatternCheckingNYI.agda | 20 -
test/fail/CopatternCheckingNYI.err | 6 -
test/fail/CopatternNonterminating.agda | 57 -
test/fail/CopatternNonterminating.err | 8 -
test/fail/CopatternWithoutFieldName.agda | 15 -
test/fail/CopatternWithoutFieldName.err | 4 -
...ctPrintingOfVariablesInSortCheckingForData.agda | 19 -
...ectPrintingOfVariablesInSortCheckingForData.err | 3 -
test/fail/Crash.agda | 22 -
test/fail/Crash.err | 3 -
test/fail/CyclicModuleDependency.agda | 4 -
test/fail/CyclicModuleDependency.err | 6 -
test/fail/DataParameterPolarity.agda | 28 -
test/fail/DataParameterPolarity.err | 3 -
test/fail/DataRecordCoinductive.agda | 38 -
test/fail/DataRecordCoinductive.err | 6 -
test/fail/DifferentArities.agda | 11 -
test/fail/DifferentArities.err | 3 -
test/fail/DoNotFireLiteralCatchAllForNeutrals.agda | 20 -
test/fail/DoNotFireLiteralCatchAllForNeutrals.err | 3 -
test/fail/DontPrune.agda | 23 -
test/fail/DontPrune.err | 5 -
test/fail/DuplicateBuiltinBinding.agda | 7 -
test/fail/DuplicateBuiltinBinding.err | 4 -
test/fail/DuplicateConstructors.agda | 9 -
test/fail/DuplicateConstructors.err | 6 -
test/fail/DuplicateFields.agda | 11 -
test/fail/DuplicateFields.err | 4 -
test/fail/EmptyInductiveRecord.agda | 29 -
test/fail/EmptyInductiveRecord.err | 8 -
test/fail/ExistentialsProjections.agda | 24 -
test/fail/ExistentialsProjections.err | 3 -
.../FakeProjectionsDoNotPreserveGuardedness.agda | 34 -
.../FakeProjectionsDoNotPreserveGuardedness.err | 10 -
test/fail/FileNotFound.agda | 3 -
test/fail/FileNotFound.err | 9 -
test/fail/FixityOutOfScopeInRecord.agda | 5 -
test/fail/FixityOutOfScopeInRecord.err | 2 -
test/fail/FrozenMVar.agda | 18 -
test/fail/FrozenMVar.err | 4 -
test/fail/FrozenMVar2.agda | 48 -
test/fail/FrozenMVar2.err | 3 -
test/fail/IllegalUseOfIrrelevantDeclaration.agda | 18 -
test/fail/IllegalUseOfIrrelevantDeclaration.err | 5 -
test/fail/IlltypedPattern.agda | 10 -
test/fail/IlltypedPattern.err | 3 -
test/fail/ImplicitRecordFields.agda | 31 -
test/fail/ImplicitRecordFields.err | 3 -
test/fail/ImportInMutual.agda | 10 -
test/fail/ImportInMutual.err | 2 -
test/fail/Imports/.cvsignore | 1 -
test/fail/Imports/A.agda | 5 -
test/fail/Imports/Ambiguous.agda | 0
test/fail/Imports/Ambiguous.lagda | 0
test/fail/Imports/B.agda | 5 -
test/fail/Imports/Bool.agda | 5 -
test/fail/Imports/Coinduction.agda | 16 -
test/fail/Imports/Level.agda | 19 -
test/fail/Imports/NonTerminating.agda | 4 -
test/fail/Imports/ShouldBePi.agda | 5 -
test/fail/Imports/Test.agda | 7 -
test/fail/Imports/Unsolved.agda | 6 -
test/fail/Impossible.agda | 5 -
test/fail/Impossible.err | 2 -
test/fail/IncompletePatternMatching.agda | 19 -
test/fail/IncompletePatternMatching.err | 5 -
test/fail/IndentedCheckingMessages.agda | 6 -
test/fail/IndentedCheckingMessages.err | 12 -
test/fail/IndentedCheckingMessages.flags | 1 -
test/fail/InductiveAndCoinductiveConstructors.err | 7 -
test/fail/InferRecordTypes-1.agda | 5 -
test/fail/InferRecordTypes-1.err | 3 -
test/fail/InferRecordTypes-2.agda | 10 -
test/fail/InferRecordTypes-2.err | 3 -
test/fail/InferRecordTypes-3.agda | 17 -
test/fail/InferRecordTypes-3.err | 4 -
test/fail/InferRecordTypes-4.agda | 17 -
test/fail/InferRecordTypes-4.err | 4 -
.../fail/Inference-of-implicit-function-space.agda | 18 -
test/fail/Inference-of-implicit-function-space.err | 4 -
test/fail/InjectiveTypeConstructors.agda | 10 -
test/fail/InjectiveTypeConstructors.err | 3 -
test/fail/InstanceArgumentsAmbiguous.agda | 8 -
test/fail/InstanceArgumentsAmbiguous.err | 3 -
test/fail/InstanceArgumentsBraceSpaces.agda | 5 -
test/fail/InstanceArgumentsBraceSpaces.err | 3 -
.../fail/InstanceArgumentsModNotParameterised.agda | 14 -
test/fail/InstanceArgumentsModNotParameterised.err | 4 -
test/fail/InstanceArgumentsNotFound.agda | 7 -
test/fail/InstanceArgumentsNotFound.err | 3 -
test/fail/Interaction-and-input-file.agda | 1 -
test/fail/Interaction-and-input-file.err | 48 -
test/fail/Interaction-and-input-file.flags | 1 -
test/fail/IrrelevantData.agda | 10 -
test/fail/IrrelevantData.err | 3 -
test/fail/IrrelevantFamilyIndex.agda | 40 -
test/fail/IrrelevantFamilyIndex.err | 3 -
test/fail/IrrelevantFin.agda | 14 -
test/fail/IrrelevantFin.err | 3 -
test/fail/IrrelevantIndexNotInconsistent.agda | 29 -
test/fail/IrrelevantIndexNotInconsistent.err | 3 -
test/fail/IrrelevantLambda.agda | 9 -
test/fail/IrrelevantLambda.err | 3 -
test/fail/IrrelevantLevelHurkens.agda | 83 -
test/fail/IrrelevantLevelHurkens.err | 3 -
test/fail/IrrelevantLevelToSet.agda | 9 -
test/fail/IrrelevantLevelToSet.err | 3 -
test/fail/IrrelevantMatchRefl.agda | 60 -
test/fail/IrrelevantMatchRefl.err | 3 -
test/fail/IrrelevantModuleParameter.agda | 5 -
test/fail/IrrelevantModuleParameter.err | 3 -
test/fail/IrrelevantModuleParameter1.agda | 6 -
test/fail/IrrelevantModuleParameter1.err | 3 -
test/fail/IrrelevantProjections.agda | 12 -
test/fail/IrrelevantProjections.err | 4 -
test/fail/IrrelevantRecordField.agda | 11 -
test/fail/IrrelevantRecordField.err | 3 -
test/fail/IrrelevantRecordMatching.agda | 13 -
test/fail/IrrelevantRecordMatching.err | 3 -
test/fail/IrrelevantTelescope.agda | 7 -
test/fail/IrrelevantTelescope.err | 3 -
test/fail/IrrelevantTelescopeRecord.agda | 8 -
test/fail/IrrelevantTelescopeRecord.err | 3 -
test/fail/IrrelevantVar.agda | 8 -
test/fail/IrrelevantVar.err | 3 -
test/fail/Issue113.agda | 14 -
test/fail/Issue113.err | 3 -
test/fail/Issue118Comment9.agda | 45 -
test/fail/Issue118Comment9.err | 6 -
test/fail/Issue121.agda | 17 -
test/fail/Issue121.err | 4 -
test/fail/Issue127.agda | 20 -
test/fail/Issue127.err | 3 -
test/fail/Issue138.err | 2 -
test/fail/Issue154.agda | 9 -
test/fail/Issue154.err | 5 -
test/fail/Issue160.agda | 16 -
test/fail/Issue160.err | 3 -
test/fail/Issue183.agda | 23 -
test/fail/Issue183.err | 3 -
test/fail/Issue202.agda | 16 -
test/fail/Issue202.err | 4 -
test/fail/Issue203.agda | 9 -
test/fail/Issue203.err | 4 -
test/fail/Issue203b.agda | 14 -
test/fail/Issue203b.err | 4 -
test/fail/Issue205.agda | 12 -
test/fail/Issue205.err | 3 -
test/fail/Issue206.agda | 18 -
test/fail/Issue206.err | 4 -
test/fail/Issue215.agda | 6 -
test/fail/Issue215.err | 4 -
test/fail/Issue216.agda | 16 -
test/fail/Issue216.err | 3 -
test/fail/Issue217.agda | 6 -
test/fail/Issue217.err | 5 -
test/fail/Issue228.agda | 36 -
test/fail/Issue228.err | 3 -
test/fail/Issue249-2.agda | 13 -
test/fail/Issue249-2.err | 4 -
test/fail/Issue249.agda | 13 -
test/fail/Issue249.err | 4 -
test/fail/Issue256.agda | 18 -
test/fail/Issue256.err | 6 -
test/fail/Issue260a.agda | 5 -
test/fail/Issue260a.err | 5 -
test/fail/Issue260b.agda | 5 -
test/fail/Issue260b.err | 5 -
test/fail/Issue260c.agda | 5 -
test/fail/Issue260c.err | 5 -
test/fail/Issue260d.agda | 5 -
test/fail/Issue260d.err | 5 -
test/fail/Issue274.agda | 13 -
test/fail/Issue274.err | 3 -
test/fail/Issue278.agda | 11 -
test/fail/Issue278.err | 3 -
test/fail/Issue279-2.agda | 20 -
test/fail/Issue279-2.err | 3 -
test/fail/Issue279.agda | 20 -
test/fail/Issue279.err | 3 -
test/fail/Issue280.agda | 9 -
test/fail/Issue280.err | 3 -
test/fail/Issue291a.agda | 15 -
test/fail/Issue291a.err | 3 -
test/fail/Issue291b.agda | 16 -
test/fail/Issue291b.err | 3 -
test/fail/Issue292.agda | 42 -
test/fail/Issue292.err | 4 -
test/fail/Issue292b.err | 4 -
test/fail/Issue292c.agda | 47 -
test/fail/Issue292c.err | 3 -
test/fail/Issue292d.agda | 33 -
test/fail/Issue292d.err | 8 -
test/fail/Issue295.agda | 29 -
test/fail/Issue295.err | 4 -
test/fail/Issue308a.agda | 9 -
test/fail/Issue308a.err | 4 -
test/fail/Issue308b.agda | 9 -
test/fail/Issue308b.err | 4 -
test/fail/Issue309a.agda | 9 -
test/fail/Issue309a.err | 4 -
test/fail/Issue309b.agda | 9 -
test/fail/Issue309b.err | 4 -
test/fail/Issue318.agda | 10 -
test/fail/Issue318.err | 5 -
test/fail/Issue328.agda | 8 -
test/fail/Issue328.err | 2 -
test/fail/Issue329.agda | 6 -
test/fail/Issue329.err | 2 -
test/fail/Issue329b.agda | 6 -
test/fail/Issue329b.err | 2 -
test/fail/Issue329c.agda | 6 -
test/fail/Issue329c.err | 2 -
test/fail/Issue332.agda | 10 -
test/fail/Issue332.err | 5 -
test/fail/Issue334.agda | 21 -
test/fail/Issue334.err | 6 -
test/fail/Issue347.agda | 35 -
test/fail/Issue347.err | 3 -
test/fail/Issue351a.agda | 15 -
test/fail/Issue351a.err | 3 -
test/fail/Issue357.agda | 20 -
test/fail/Issue357.err | 4 -
test/fail/Issue380.agda | 31 -
test/fail/Issue380.err | 5 -
test/fail/Issue381.agda | 13 -
test/fail/Issue381.err | 3 -
test/fail/Issue390.agda | 3 -
test/fail/Issue390.err | 3 -
test/fail/Issue390.flags | 1 -
test/fail/Issue392.agda | 30 -
test/fail/Issue392.err | 3 -
test/fail/Issue399.agda | 41 -
test/fail/Issue399.err | 9 -
test/fail/Issue402.agda | 16 -
test/fail/Issue402.err | 3 -
test/fail/Issue413.agda | 14 -
test/fail/Issue413.err | 8 -
test/fail/Issue418.agda | 21 -
test/fail/Issue418.err | 4 -
test/fail/Issue424.agda | 16 -
test/fail/Issue424.err | 2 -
test/fail/Issue427.agda | 18 -
test/fail/Issue427.err | 4 -
test/fail/Issue444.agda | 12 -
test/fail/Issue444.err | 6 -
test/fail/Issue452.agda | 42 -
test/fail/Issue452.err | 3 -
test/fail/Issue461.agda | 5 -
test/fail/Issue461.err | 5 -
test/fail/Issue464.agda | 35 -
test/fail/Issue464.err | 4 -
test/fail/Issue476a.agda | 6 -
test/fail/Issue476a.err | 3 -
test/fail/Issue476b.agda | 7 -
test/fail/Issue476b.err | 3 -
test/fail/Issue476c.agda | 12 -
test/fail/Issue476c.err | 4 -
test/fail/Issue476d.agda | 12 -
test/fail/Issue476d.err | 4 -
test/fail/Issue477.agda | 5 -
test/fail/Issue477.err | 2 -
test/fail/Issue477b.agda | 5 -
test/fail/Issue477b.err | 2 -
test/fail/Issue478.agda | 24 -
test/fail/Issue478.err | 3 -
test/fail/Issue478b.agda | 11 -
test/fail/Issue478b.err | 3 -
test/fail/Issue478c.agda | 13 -
test/fail/Issue478c.err | 3 -
test/fail/Issue481.agda | 10 -
test/fail/Issue481.err | 6 -
test/fail/Issue481InstantiatedImportOnly.agda | 4 -
test/fail/Issue481InstantiatedImportOnly.err | 6 -
test/fail/Issue481NonExistentModule.agda | 8 -
test/fail/Issue481NonExistentModule.err | 9 -
test/fail/Issue481a.agda | 10 -
test/fail/Issue481a.err | 4 -
test/fail/Issue483.agda | 29 -
test/fail/Issue483.err | 4 -
test/fail/Issue483a.agda | 28 -
test/fail/Issue483a.err | 4 -
test/fail/Issue483b.agda | 18 -
test/fail/Issue483b.err | 4 -
test/fail/Issue483c.agda | 24 -
test/fail/Issue483c.err | 4 -
test/fail/Issue484.agda | 10 -
test/fail/Issue484.err | 4 -
test/fail/Issue485.agda | 6 -
test/fail/Issue485.err | 3 -
test/fail/Issue503.agda | 45 -
test/fail/Issue503.err | 6 -
test/fail/Issue512.agda | 31 -
test/fail/Issue512.err | 5 -
test/fail/Issue526.agda | 24 -
test/fail/Issue526.err | 9 -
test/fail/Issue530.agda | 20 -
test/fail/Issue530.err | 4 -
test/fail/Issue543.agda | 44 -
test/fail/Issue543.err | 5 -
test/fail/Issue546.agda | 21 -
test/fail/Issue546.err | 3 -
test/fail/Issue549.agda | 8 -
test/fail/Issue549.err | 3 -
test/fail/Issue551.agda | 36 -
test/fail/Issue551.err | 3 -
test/fail/Issue551a.agda | 16 -
test/fail/Issue551a.err | 3 -
test/fail/Issue555.agda | 6 -
test/fail/Issue555.err | 2 -
test/fail/Issue555a.agda | 19 -
test/fail/Issue555a.err | 2 -
test/fail/Issue555b.agda | 20 -
test/fail/Issue555b.err | 2 -
test/fail/Issue555c.agda | 8 -
test/fail/Issue555c.err | 2 -
test/fail/Issue562.agda | 11 -
test/fail/Issue562.err | 5 -
test/fail/Issue580.agda | 5 -
test/fail/Issue580.err | 4 -
test/fail/Issue585-11.agda | 27 -
test/fail/Issue585-11.err | 4 -
test/fail/Issue585.agda | 62 -
test/fail/Issue585.err | 5 -
test/fail/Issue585t.agda | 31 -
test/fail/Issue585t.err | 4 -
test/fail/Issue586.agda | 5 -
test/fail/Issue586.err | 2 -
test/fail/Issue586.flags | 1 -
test/fail/Issue610-4.agda | 37 -
test/fail/Issue610-4.err | 3 -
test/fail/Issue610.agda | 36 -
test/fail/Issue610.err | 4 -
test/fail/Issue62.agda | 22 -
test/fail/Issue62.err | 3 -
test/fail/Issue628.agda | 27 -
test/fail/Issue628.err | 4 -
test/fail/Issue631.agda | 21 -
test/fail/Issue631.err | 3 -
test/fail/Issue636.agda | 19 -
test/fail/Issue636.err | 6 -
test/fail/Issue644.agda | 37 -
test/fail/Issue644.err | 3 -
test/fail/Issue659.agda | 53 -
test/fail/Issue659.err | 4 -
test/fail/Issue676.agda | 23 -
test/fail/Issue676.err | 4 -
test/fail/Issue689.agda | 10 -
test/fail/Issue689.err | 4 -
test/fail/Issue690.agda | 28 -
test/fail/Issue690.err | 4 -
test/fail/Issue690a.agda | 6 -
test/fail/Issue690a.err | 3 -
test/fail/Issue691.agda | 28 -
test/fail/Issue691.err | 4 -
test/fail/Issue705.agda | 8 -
test/fail/Issue705.err | 6 -
test/fail/Issue719.agda | 12 -
test/fail/Issue719.err | 5 -
test/fail/Issue721a.agda | 16 -
test/fail/Issue721a.err | 4 -
test/fail/Issue721b.agda | 17 -
test/fail/Issue721b.err | 3 -
test/fail/Issue721c.agda | 24 -
test/fail/Issue721c.err | 3 -
test/fail/Issue723.agda | 47 -
test/fail/Issue723.err | 6 -
test/fail/Issue735.agda | 24 -
test/fail/Issue735.err | 4 -
test/fail/Issue738.agda | 58 -
test/fail/Issue738.err | 8 -
test/fail/Issue87.agda | 13 -
test/fail/Issue87.err | 7 -
test/fail/JasonReedPruning.agda | 35 -
test/fail/JasonReedPruning.err | 3 -
test/fail/LetPair.agda | 18 -
test/fail/LetPair.err | 3 -
test/fail/LevelLiterals.agda | 13 -
test/fail/LevelLiterals.err | 3 -
test/fail/LevelUnification.agda | 14 -
test/fail/LevelUnification.err | 3 -
test/fail/LocalVsImportedModuleClash.agda | 4 -
test/fail/LocalVsImportedModuleClash.err | 6 -
test/fail/LostTypeError.agda | 23 -
test/fail/LostTypeError.err | 3 -
test/fail/LostTypeError2.agda | 25 -
test/fail/LostTypeError2.err | 3 -
test/fail/MagicWith.agda | 37 -
test/fail/MagicWith.err | 5 -
test/fail/Makefile | 165 -
test/fail/MalformedModuleNameInIMPORT.agda | 3 -
test/fail/MalformedModuleNameInIMPORT.err | 3 -
test/fail/MatchOnIrrelevantData1.agda | 21 -
test/fail/MatchOnIrrelevantData1.err | 3 -
test/fail/MetaAppUnderLambda.agda | 21 -
test/fail/MetaAppUnderLambda.err | 4 -
test/fail/MetaCannotDependOn.agda | 14 -
test/fail/MetaCannotDependOn.err | 6 -
test/fail/MetaOccursInItself.agda | 16 -
test/fail/MetaOccursInItself.err | 3 -
test/fail/MisformedTypeSignature.agda | 5 -
test/fail/MisformedTypeSignature.err | 3 -
test/fail/MissingDefinition.agda | 5 -
test/fail/MissingDefinition.err | 2 -
test/fail/MissingTypeSignature.agda | 10 -
test/fail/MissingTypeSignature.err | 4 -
test/fail/MissingTypeSignatureInMutual.agda | 11 -
test/fail/MissingTypeSignatureInMutual.err | 2 -
test/fail/MissingWithClauses.agda | 7 -
test/fail/MissingWithClauses.err | 2 -
test/fail/ModuleArityMismatch.agda | 8 -
test/fail/ModuleArityMismatch.err | 3 -
test/fail/ModuleDefinedInOtherFile.agda | 5 -
test/fail/ModuleDefinedInOtherFile.err | 8 -
test/fail/ModuleDoesntExport.agda | 7 -
test/fail/ModuleDoesntExport.err | 4 -
test/fail/ModuleInMutual.agda | 14 -
test/fail/ModuleInMutual.err | 2 -
test/fail/ModuleNameDoesntMatchFileName.agda | 1 -
test/fail/ModuleNameDoesntMatchFileName.err | 8 -
test/fail/MultipleFixityDecl.agda | 9 -
test/fail/MultipleFixityDecl.err | 7 -
test/fail/NaturalAndLevelDifferent.agda | 8 -
test/fail/NaturalAndLevelDifferent.err | 3 -
test/fail/NeedOptionCopatterns.agda | 13 -
test/fail/NeedOptionCopatterns.err | 3 -
test/fail/Negative1.agda | 5 -
test/fail/Negative1.err | 3 -
test/fail/Negative2.agda | 9 -
test/fail/Negative2.err | 4 -
test/fail/Negative3.agda | 6 -
test/fail/Negative3.err | 4 -
test/fail/Negative4.agda | 9 -
test/fail/Negative4.err | 3 -
test/fail/Negative5.agda | 5 -
test/fail/Negative5.err | 5 -
test/fail/NoBindingForBuiltin.agda | 4 -
test/fail/NoBindingForBuiltin.err | 4 -
test/fail/NoNoTerminationCheck.agda | 14 -
test/fail/NoNoTerminationCheck.err | 5 -
test/fail/NoPanic.agda | 31 -
test/fail/NoPanic.err | 4 -
test/fail/NoParseForApplication.agda | 13 -
test/fail/NoParseForApplication.err | 3 -
test/fail/NoParseForLHS.agda | 14 -
test/fail/NoParseForLHS.err | 4 -
test/fail/NoRHSRequiresAbsurdPattern.agda | 12 -
test/fail/NoRHSRequiresAbsurdPattern.err | 4 -
test/fail/NoSuchBuiltinName.agda | 6 -
test/fail/NoSuchBuiltinName.err | 3 -
test/fail/NoSuchModule.agda | 3 -
test/fail/NoSuchModule.err | 4 -
test/fail/NoSuchPrimitiveFunction.agda | 7 -
test/fail/NoSuchPrimitiveFunction.err | 3 -
test/fail/NoTerminationCheck1.agda | 6 -
test/fail/NoTerminationCheck1.err | 3 -
test/fail/NoTerminationCheck2.agda | 8 -
test/fail/NoTerminationCheck2.err | 3 -
test/fail/NoTerminationCheck3.agda | 12 -
test/fail/NoTerminationCheck3.err | 4 -
test/fail/NoTerminationCheck4.agda | 13 -
test/fail/NoTerminationCheck4.err | 3 -
test/fail/NonDependentConstructorType.agda | 10 -
test/fail/NonDependentConstructorType.err | 3 -
test/fail/NonLinearConstraint.agda | 10 -
test/fail/NonLinearConstraint.err | 4 -
test/fail/NotAModuleExpr.agda | 6 -
test/fail/NotAModuleExpr.err | 3 -
test/fail/NotAValidLetBinding.agda | 11 -
test/fail/NotAValidLetBinding.err | 7 -
test/fail/NotAnExpression.agda | 6 -
test/fail/NotAnExpression.err | 3 -
...NotApplyingInDontCareTriggersInternalError.agda | 62 -
.../NotApplyingInDontCareTriggersInternalError.err | 3 -
test/fail/NotInScope.agda | 10 -
test/fail/NotInScope.err | 5 -
test/fail/NotLeqSort.agda | 6 -
test/fail/NotLeqSort.err | 4 -
test/fail/NotStrictlyPositive.agda | 14 -
test/fail/NotStrictlyPositive.err | 4 -
test/fail/NotStrictlyPositiveInMutual.agda | 10 -
test/fail/NotStrictlyPositiveInMutual.err | 5 -
test/fail/NotStronglyRigidOccurrence.agda | 18 -
test/fail/NotStronglyRigidOccurrence.err | 4 -
test/fail/NothingAppliedToHiddenArg.agda | 4 -
test/fail/NothingAppliedToHiddenArg.err | 4 -
test/fail/OccursCheck.agda | 14 -
test/fail/OccursCheck.err | 3 -
test/fail/OccursCheck1.agda | 19 -
test/fail/OccursCheck1.err | 3 -
test/fail/OpenInMutual.agda | 12 -
test/fail/OpenInMutual.err | 2 -
test/fail/OpenPublicPlusTypeError.agda | 12 -
test/fail/OpenPublicPlusTypeError.err | 3 -
test/fail/ParseError.agda | 1 -
test/fail/ParseError.err | 3 -
test/fail/ParseForallAbsurd.agda | 8 -
test/fail/ParseForallAbsurd.err | 3 -
test/fail/PatternMatchingOnCodata.agda | 31 -
test/fail/PatternMatchingOnCodata.err | 4 -
test/fail/PatternShadowsConstructor.agda | 14 -
test/fail/PatternShadowsConstructor.err | 3 -
test/fail/PatternShadowsConstructor2.agda | 13 -
test/fail/PatternShadowsConstructor2.err | 3 -
test/fail/PatternSynonymAmbiguousParse.agda | 8 -
test/fail/PatternSynonymAmbiguousParse.err | 7 -
test/fail/PatternSynonymMutualBlock.agda | 7 -
test/fail/PatternSynonymMutualBlock.err | 2 -
test/fail/PatternSynonymNoParse.agda | 3 -
test/fail/PatternSynonymNoParse.err | 4 -
test/fail/PatternSynonymOverapplied.agda | 10 -
test/fail/PatternSynonymOverapplied.err | 3 -
test/fail/PatternSynonymOverapplied2.agda | 11 -
test/fail/PatternSynonymOverapplied2.err | 4 -
test/fail/PatternSynonymOverloaded.agda | 8 -
test/fail/PatternSynonymOverloaded.err | 5 -
test/fail/PatternSynonymParameterisedModule.agda | 14 -
test/fail/PatternSynonymParameterisedModule.err | 4 -
test/fail/PatternSynonymUnderapplied.agda | 11 -
test/fail/PatternSynonymUnderapplied.err | 4 -
test/fail/PatternSynonymsErrorLocation.agda | 69 -
test/fail/PatternSynonymsErrorLocation.err | 3 -
test/fail/PositivityCheckNeedsLinearityCheck.agda | 30 -
test/fail/PositivityCheckNeedsLinearityCheck.err | 3 -
test/fail/PostulateInMutual.agda | 9 -
test/fail/PostulateInMutual.err | 2 -
test/fail/PragmaInMutual.agda | 14 -
test/fail/PragmaInMutual.err | 2 -
test/fail/PragmasApplyOnlyToCurrentModule.agda | 5 -
test/fail/PragmasApplyOnlyToCurrentModule.err | 8 -
test/fail/PrimitiveInMutual.agda | 14 -
test/fail/PrimitiveInMutual.err | 2 -
test/fail/Productivity.agda | 51 -
test/fail/Productivity.err | 16 -
test/fail/PropNoMore.agda | 5 -
test/fail/PropNoMore.err | 3 -
test/fail/PruningNonMillerPatternFail.agda | 24 -
test/fail/PruningNonMillerPatternFail.err | 7 -
test/fail/PublicWithoutOpen.agda | 5 -
test/fail/PublicWithoutOpen.err | 4 -
test/fail/PublicWithoutOpen2.agda | 3 -
test/fail/PublicWithoutOpen2.err | 4 -
test/fail/PureLambda.agda | 15 -
test/fail/PureLambda.err | 3 -
test/fail/RecordConstructorOutOfScope.agda | 7 -
test/fail/RecordConstructorOutOfScope.err | 5 -
test/fail/RecordConstructorsInErrorMessages.agda | 32 -
test/fail/RecordConstructorsInErrorMessages.err | 3 -
test/fail/RecordUpdatePreservesType.agda | 18 -
test/fail/RecordUpdatePreservesType.err | 3 -
test/fail/ReifyProjectionLike.agda | 32 -
test/fail/ReifyProjectionLike.err | 4 -
test/fail/RepeatedVariableInPattern.agda | 6 -
test/fail/RepeatedVariableInPattern.err | 3 -
test/fail/Rewrite.agda | 13 -
test/fail/Rewrite.err | 4 -
test/fail/SafeFlagNoTermination.agda | 7 -
test/fail/SafeFlagNoTermination.err | 2 -
test/fail/SafeFlagNoTermination.flags | 1 -
test/fail/SafeFlagPostulate.agda | 5 -
test/fail/SafeFlagPostulate.err | 4 -
test/fail/SafeFlagPostulate.flags | 1 -
test/fail/SafeFlagPragmas.agda | 11 -
test/fail/SafeFlagPragmas.err | 6 -
test/fail/SafeFlagPragmas.flags | 1 -
test/fail/SafeFlagPrimTrustMe.agda | 9 -
test/fail/SafeFlagPrimTrustMe.err | 4 -
test/fail/SafeFlagPrimTrustMe.flags | 1 -
test/fail/ScopeIrrelevantRecordField.agda | 10 -
test/fail/ScopeIrrelevantRecordField.err | 5 -
test/fail/SetOmega.agda | 9 -
test/fail/SetOmega.err | 5 -
test/fail/ShadowModule.agda | 10 -
test/fail/ShadowModule.err | 5 -
test/fail/ShadowModule2.agda | 11 -
test/fail/ShadowModule2.err | 6 -
test/fail/ShapeIrrelevantIndex.agda | 13 -
test/fail/ShapeIrrelevantIndex.err | 3 -
.../ShapeIrrelevantIndexNoBecauseOfRecursion.agda | 29 -
.../ShapeIrrelevantIndexNoBecauseOfRecursion.err | 3 -
...apeIrrelevantParameterNoBecauseOfRecursion.agda | 25 -
...hapeIrrelevantParameterNoBecauseOfRecursion.err | 3 -
test/fail/ShouldBeASort.agda | 6 -
test/fail/ShouldBeASort.err | 5 -
test/fail/ShouldBeApplicationOf.agda | 9 -
test/fail/ShouldBeApplicationOf.err | 3 -
.../ShouldBeAppliedToTheDatatypeParameters.agda | 16 -
.../ShouldBeAppliedToTheDatatypeParameters.err | 3 -
test/fail/ShouldBeEmpty.agda | 13 -
test/fail/ShouldBeEmpty.err | 5 -
test/fail/ShouldBePi.agda | 15 -
test/fail/ShouldBePi.err | 3 -
test/fail/ShouldEndInApplicationOfTheDatatype.agda | 16 -
test/fail/ShouldEndInApplicationOfTheDatatype.err | 4 -
.../SizeUnsolvedConstraintsInTypeSignature.agda | 24 -
.../SizeUnsolvedConstraintsInTypeSignature.err | 3 -
test/fail/SizedTypesFunctionFromSuccSize.agda | 21 -
test/fail/SizedTypesFunctionFromSuccSize.err | 6 -
test/fail/SizedTypesRigidVarClash.agda | 19 -
test/fail/SizedTypesRigidVarClash.err | 3 -
test/fail/SizedTypesScopeExtrusion.agda | 28 -
test/fail/SizedTypesScopeExtrusion.err | 3 -
test/fail/SizedTypesVarSwap.agda | 20 -
test/fail/SizedTypesVarSwap.err | 6 -
.../SkipParametersInConstructorReification.agda | 26 -
.../SkipParametersInConstructorReification.err | 4 -
test/fail/SortDependingOnIndex.agda | 6 -
test/fail/SortDependingOnIndex.err | 4 -
test/fail/SplitOnIrrelevant.agda | 11 -
test/fail/SplitOnIrrelevant.err | 3 -
test/fail/StrangeRecursiveUnquote.agda | 12 -
test/fail/StrangeRecursiveUnquote.err | 4 -
test/fail/StronglyRigidOccurrence.agda | 14 -
test/fail/StronglyRigidOccurrence.err | 3 -
test/fail/SubjectReduction.agda | 39 -
test/fail/SubjectReduction.err | 5 -
test/fail/SyntaxForOperators.agda | 5 -
test/fail/SyntaxForOperators.err | 4 -
test/fail/Tabs.agda | 6 -
test/fail/Tabs.err | 4 -
test/fail/TabsInPragmas.agda | 3 -
test/fail/TabsInPragmas.err | 4 -
test/fail/TermSplicing1.agda | 6 -
test/fail/TermSplicing1.err | 3 -
test/fail/TermSplicingLooping.agda | 8 -
test/fail/TermSplicingLooping.err | 5 -
test/fail/TermSplicingOutOfScope.agda | 7 -
test/fail/TermSplicingOutOfScope.err | 3 -
test/fail/TerminationInfiniteRecord.agda | 15 -
test/fail/TerminationInfiniteRecord.err | 6 -
test/fail/TerminationLambda.agda | 9 -
test/fail/TerminationLambda.err | 6 -
test/fail/TerminationNoArgs.agda | 4 -
test/fail/TerminationNoArgs.err | 6 -
test/fail/TerminationOnIrrelevant.agda | 24 -
test/fail/TerminationOnIrrelevant.err | 3 -
test/fail/TerminationRecordPatternCoerce.agda | 58 -
test/fail/TerminationRecordPatternCoerce.err | 8 -
test/fail/TerminationRecordPatternLie.agda | 45 -
test/fail/TerminationRecordPatternLie.err | 8 -
test/fail/TerminationRecordPatternListAppend.agda | 41 -
test/fail/TerminationRecordPatternListAppend.err | 3 -
test/fail/TerminationWithInsufficientDepth.agda | 21 -
test/fail/TerminationWithInsufficientDepth.err | 7 -
test/fail/TerminationWithMerge.agda | 31 -
test/fail/TerminationWithMerge.err | 3 -
test/fail/TooManyArgumentsInLHS.agda | 6 -
test/fail/TooManyArgumentsInLHS.err | 4 -
test/fail/TooManyFields.agda | 11 -
test/fail/TooManyFields.err | 4 -
test/fail/TrustMe.agda | 21 -
test/fail/TrustMe.err | 3 -
test/fail/TwoCompilers.agda | 1 -
test/fail/TwoCompilers.err | 40 -
test/fail/TwoCompilers.flags | 1 -
.../TypeConstructorsWhichPreserveGuardedness1.agda | 67 -
.../TypeConstructorsWhichPreserveGuardedness1.err | 12 -
.../TypeConstructorsWhichPreserveGuardedness2.agda | 14 -
.../TypeConstructorsWhichPreserveGuardedness2.err | 5 -
.../TypeConstructorsWhichPreserveGuardedness3.agda | 12 -
.../TypeConstructorsWhichPreserveGuardedness3.err | 5 -
.../TypeConstructorsWhichPreserveGuardedness4.agda | 20 -
.../TypeConstructorsWhichPreserveGuardedness4.err | 7 -
test/fail/UnequalHiding.agda | 7 -
test/fail/UnequalHiding.err | 6 -
test/fail/UnequalRelevance.agda | 11 -
test/fail/UnequalRelevance.err | 4 -
test/fail/UnequalSorts.agda | 9 -
test/fail/UnequalSorts.err | 3 -
test/fail/UnequalTerms.agda | 12 -
test/fail/UnequalTerms.err | 3 -
...tionUndecidedForNonStronglyRigidOccurrence.agda | 15 -
...ationUndecidedForNonStronglyRigidOccurrence.err | 3 -
test/fail/UnifyWithIrrelevantArgument.agda | 12 -
test/fail/UnifyWithIrrelevantArgument.err | 5 -
test/fail/UninstantiatedDotPattern.agda | 6 -
test/fail/UninstantiatedDotPattern.err | 3 -
test/fail/UnknownNameInFixityDecl.agda | 6 -
test/fail/UnknownNameInFixityDecl.err | 2 -
test/fail/UnquoteSetOmega.agda | 19 -
test/fail/UnquoteSetOmega.err | 3 -
test/fail/Unreachable.agda | 23 -
test/fail/Unreachable.err | 3 -
test/fail/UnsolvableLevelConstraintsInDataDef.agda | 7 -
test/fail/UnsolvableLevelConstraintsInDataDef.err | 4 -
test/fail/Unsolved-meta-in-module-application.agda | 5 -
test/fail/Unsolved-meta-in-module-application.err | 3 -
test/fail/Unsolved-meta-in-module-telescope.agda | 1 -
test/fail/Unsolved-meta-in-module-telescope.err | 3 -
test/fail/Unsolved-meta-in-postulate.agda | 3 -
test/fail/Unsolved-meta-in-postulate.err | 3 -
test/fail/UnsolvedMetas.agda | 5 -
test/fail/UnsolvedMetas.err | 4 -
test/fail/WhyWeNeedUntypedLambda.agda | 21 -
test/fail/WhyWeNeedUntypedLambda.err | 5 -
test/fail/WithScopeError.agda | 12 -
test/fail/WithScopeError.err | 5 -
test/fail/WithoutK1.agda | 13 -
test/fail/WithoutK1.err | 10 -
test/fail/WithoutK10.agda | 12 -
test/fail/WithoutK10.err | 11 -
test/fail/WithoutK2.agda | 13 -
test/fail/WithoutK2.err | 10 -
test/fail/WithoutK3.agda | 36 -
test/fail/WithoutK3.err | 11 -
test/fail/WithoutK4.agda | 10 -
test/fail/WithoutK4.err | 6 -
test/fail/WithoutK5.agda | 11 -
test/fail/WithoutK5.err | 12 -
test/fail/WithoutK6.agda | 12 -
test/fail/WithoutK6.err | 12 -
test/fail/WithoutK7.agda | 14 -
test/fail/WithoutK7.err | 10 -
test/fail/WithoutK8.agda | 20 -
test/fail/WithoutK8.err | 6 -
test/fail/WithoutK9.agda | 17 -
test/fail/WithoutK9.err | 12 -
test/fail/WrongDotPattern.agda | 13 -
test/fail/WrongDotPattern.err | 4 -
test/fail/WrongHidingInApplication.agda | 9 -
test/fail/WrongHidingInApplication.err | 5 -
test/fail/WrongHidingInLHS.agda | 6 -
test/fail/WrongHidingInLHS.err | 3 -
test/fail/WrongHidingInLambda.agda | 6 -
test/fail/WrongHidingInLambda.err | 4 -
test/fail/WrongMetaLeft.agda | 34 -
test/fail/WrongMetaLeft.err | 3 -
test/fail/WrongNumberOfConstructorArguments.agda | 11 -
test/fail/WrongNumberOfConstructorArguments.err | 3 -
test/fail/WrongPolarity.agda | 28 -
test/fail/WrongPolarity.err | 4 -
test/fail/WrongSizeAssignment.agda | 25 -
test/fail/WrongSizeAssignment.err | 6 -
test/fail/WrongSizeAssignment2.agda | 25 -
test/fail/WrongSizeAssignment2.err | 6 -
test/fail/customised/FFI.agda | 22 -
test/fail/customised/FFI.err | 12 -
test/fail/customised/Imports/A.agda | 1 -
test/fail/customised/NestedProjectRoots.agda | 3 -
test/fail/customised/NestedProjectRoots.err | 22 -
test/features/CoPatWith.agda | 45 -
test/features/Copatterns.agda | 74 -
test/features/FlexInterpreter.agda | 40 -
test/features/FlexibleFunArity.agda | 93 -
test/features/Makefile | 2 -
test/features/Tree.agda | 45 -
test/interaction/AutoMisc.agda | 108 -
test/interaction/AutoMisc.in | 6 -
test/interaction/AutoMisc.out | 22 -
test/interaction/Debug.agda | 5 -
test/interaction/Debug.in | 1 -
test/interaction/Debug.out | 14 -
test/interaction/Error-in-imported-module.agda | 3 -
test/interaction/Error-in-imported-module.in | 1 -
test/interaction/Error-in-imported-module.out | 9 -
test/interaction/Error-in-imported-module/M.agda | 4 -
test/interaction/ExtendedLambdaCase.agda | 30 -
test/interaction/ExtendedLambdaCase.in | 27 -
test/interaction/ExtendedLambdaCase.out | 42 -
test/interaction/GiveInSpiteOfUnsolvedIrr.agda | 46 -
test/interaction/GiveInSpiteOfUnsolvedIrr.in | 2 -
test/interaction/GiveInSpiteOfUnsolvedIrr.out | 16 -
test/interaction/GiveSize.agda | 8 -
test/interaction/GiveSize.in | 2 -
test/interaction/GiveSize.out | 13 -
test/interaction/Highlighting.agda | 24 -
test/interaction/Highlighting.in | 1 -
test/interaction/Highlighting.out | 23 -
test/interaction/Highlighting/M.agda | 1 -
test/interaction/Imports/Nat.hs | 3 -
test/interaction/Impossible.agda | 3 -
test/interaction/Impossible.in | 1 -
test/interaction/Impossible.out | 7 -
test/interaction/InferIrrelevant.agda | 7 -
test/interaction/InferIrrelevant.in | 2 -
test/interaction/InferIrrelevant.out | 12 -
test/interaction/IntroSharp.agda | 29 -
test/interaction/IntroSharp.in | 2 -
test/interaction/IntroSharp.out | 13 -
test/interaction/Issue208.agda | 5 -
test/interaction/Issue208.in | 3 -
test/interaction/Issue208.out | 12 -
test/interaction/Issue231.agda | 22 -
test/interaction/Issue231.in | 3 -
test/interaction/Issue231.out | 11 -
test/interaction/Issue254.agda | 16 -
test/interaction/Issue254.in | 4 -
test/interaction/Issue254.out | 11 -
test/interaction/Issue271.agda | 7 -
test/interaction/Issue271.in | 4 -
test/interaction/Issue271.out | 12 -
test/interaction/Issue277.agda | 18 -
test/interaction/Issue277.in | 14 -
test/interaction/Issue277.out | 21 -
test/interaction/Issue317.agda | 19 -
test/interaction/Issue317.in | 7 -
test/interaction/Issue317.out | 15 -
test/interaction/Issue358.agda | 9 -
test/interaction/Issue358.in | 4 -
test/interaction/Issue358.out | 13 -
test/interaction/Issue363.agda | 18 -
test/interaction/Issue363.in | 1 -
test/interaction/Issue363.out | 9 -
test/interaction/Issue373.agda | 62 -
test/interaction/Issue373.out | 9 -
test/interaction/Issue373.sh | 10 -
test/interaction/Issue378.agda | 21 -
test/interaction/Issue378.in | 2 -
test/interaction/Issue378.out | 13 -
test/interaction/Issue388.agda | 11 -
test/interaction/Issue388.in | 4 -
test/interaction/Issue388.out | 12 -
test/interaction/Issue417.agda | 16 -
test/interaction/Issue417.in | 7 -
test/interaction/Issue417.out | 15 -
test/interaction/Issue453.agda | 6 -
test/interaction/Issue453.in | 2 -
test/interaction/Issue453.out | 9 -
test/interaction/Issue499.agda | 14 -
test/interaction/Issue499.in | 2 -
test/interaction/Issue499.out | 11 -
test/interaction/Issue556.agda | 4 -
test/interaction/Issue556.in | 13 -
test/interaction/Issue556.out | 21 -
test/interaction/Issue564.agda | 22 -
test/interaction/Issue564.in | 2 -
test/interaction/Issue564.out | 12 -
test/interaction/Issue589.agda | 9 -
test/interaction/Issue589.in | 2 -
test/interaction/Issue589.out | 13 -
test/interaction/Issue591.agda | 3 -
test/interaction/Issue591.in | 1 -
test/interaction/Issue591.out | 11 -
test/interaction/Issue591/M.agda | 1 -
test/interaction/Issue599.agda | 13 -
test/interaction/Issue599.in | 5 -
test/interaction/Issue599.out | 18 -
test/interaction/Issue604.agda | 4 -
test/interaction/Issue604.in | 3 -
test/interaction/Issue604.out | 17 -
test/interaction/Issue606.agda | 14 -
test/interaction/Issue606.in | 3 -
test/interaction/Issue606.out | 14 -
test/interaction/Issue620.agda | 10 -
test/interaction/Issue620.in | 4 -
test/interaction/Issue620.out | 12 -
test/interaction/Issue630.agda | 9 -
test/interaction/Issue630.in | 1 -
test/interaction/Issue630.out | 9 -
test/interaction/Issue637.agda | 1 -
test/interaction/Issue637.in | 1 -
test/interaction/Issue637.out | 6 -
test/interaction/Issue639.agda | 3 -
test/interaction/Issue639.in | 1 -
test/interaction/Issue639.out | 8 -
test/interaction/Issue641.agda | 3 -
test/interaction/Issue641.out | 16 -
test/interaction/Issue641.sh | 19 -
test/interaction/Issue642.agda | 20 -
test/interaction/Issue642.in | 1 -
test/interaction/Issue642.out | 9 -
test/interaction/Issue643.agda | 24 -
test/interaction/Issue643.in | 1 -
test/interaction/Issue643.out | 9 -
test/interaction/Issue670.agda | 27 -
test/interaction/Issue670.in | 2 -
test/interaction/Issue670.out | 13 -
test/interaction/Issue679a.agda | 14 -
test/interaction/Issue679a.in | 2 -
test/interaction/Issue679a.out | 13 -
test/interaction/Issue720.agda | 1 -
test/interaction/Issue720.out | 23 -
test/interaction/Issue720.sh | 15 -
test/interaction/Literate.in | 1 -
test/interaction/Literate.lagda | 9 -
test/interaction/Literate.out | 9 -
test/interaction/Long.agda | 34 -
test/interaction/Long.in | 38 -
test/interaction/Long.out | 132 -
test/interaction/Makefile | 97 -
test/interaction/Multisplit.agda | 47 -
test/interaction/Multisplit.in | 6 -
test/interaction/Multisplit.out | 19 -
test/interaction/NiceGoals.agda | 123 -
test/interaction/NiceGoals.in | 1 -
test/interaction/NiceGoals.out | 9 -
test/interaction/Positivity-once.agda | 16 -
test/interaction/Positivity-once.in | 1 -
test/interaction/Positivity-once.out | 10 -
test/interaction/PragmasRespected.agda | 7 -
test/interaction/PragmasRespected.in | 6 -
test/interaction/PragmasRespected.out | 21 -
test/interaction/README | 29 -
test/interaction/RecordPatternMatching.agda | 21 -
test/interaction/RecordPatternMatching.in | 5 -
test/interaction/RecordPatternMatching.out | 13 -
test/interaction/RecordUpdateSyntax.agda | 11 -
test/interaction/RecordUpdateSyntax.in | 2 -
test/interaction/RecordUpdateSyntax.out | 13 -
test/interaction/SetInf.agda | 6 -
test/interaction/SetInf.in | 1 -
test/interaction/SetInf.out | 9 -
test/interaction/With-flicker.agda | 27 -
test/interaction/With-flicker.in | 1 -
test/interaction/With-flicker.out | 273 -
test/js/Makefile | 29 -
test/js/TestBool.agda | 43 -
test/js/TestHarness.agda | 21 -
test/js/TestList.agda | 42 -
test/js/TestNat.agda | 37 -
test/js/test-harness.js | 27 -
test/lib-succeed/Makefile | 45 -
test/lib-succeed/SizeInconsistentMeta4.agda | 45 -
test/succeed/.cvsignore | 2 -
test/succeed/Abstract.agda | 35 -
test/succeed/AbstractData.agda | 10 -
test/succeed/AbsurdIrrelevance.agda | 9 -
test/succeed/AbsurdLam.agda | 24 -
test/succeed/AbsurdPattern.agda | 10 -
test/succeed/Berry.agda | 19 -
test/succeed/Bush.agda | 52 -
test/succeed/CoPatStream.agda | 82 -
test/succeed/CoinductiveAfterEvaluation.agda | 17 -
test/succeed/Comments.agda | 20 -
test/succeed/CompareLevel.agda | 21 -
test/succeed/CompilingCoinduction.agda | 46 -
test/succeed/CompilingCoinduction.flags | 1 -
test/succeed/ComputedLevels.agda | 19 -
test/succeed/Const.agda | 21 -
test/succeed/Copatterns.agda | 70 -
test/succeed/CoverStrategy.agda | 33 -
test/succeed/DataPolarity.agda | 32 -
test/succeed/DataRecordInductive.agda | 65 -
test/succeed/DefinitionalEquality.agda | 26 -
test/succeed/DependentIrrelevance.agda | 52 -
test/succeed/DigitsInNames.agda | 7 -
test/succeed/Div.agda | 40 -
test/succeed/Div2.agda | 42 -
...otEtaExpandMVarsWhenComparingAgainstRecord.agda | 23 -
test/succeed/DontIgnoreIrrelevantVars.agda | 36 -
test/succeed/DotPatternTermination.agda | 46 -
test/succeed/EmptyInductiveRecord.agda | 21 -
test/succeed/Epic.agda | 32 -
test/succeed/Epic.flags | 1 -
test/succeed/EqTest.agda | 20 -
test/succeed/EtaAndMetas.agda | 18 -
test/succeed/EtaContractIrrelevant.agda | 32 -
test/succeed/EtaContractToMillerPattern.agda | 20 -
test/succeed/EtaContractionDefBody.agda | 91 -
test/succeed/Exist.agda | 29 -
.../ExplicitLambdaExperimentalIrrelevance.agda | 12 -
test/succeed/FancyRecordModule.agda | 27 -
test/succeed/Filter.agda | 32 -
test/succeed/FilterSub.agda | 59 -
test/succeed/FlexRemoval.agda | 54 -
test/succeed/ForallForParameters.agda | 20 -
test/succeed/FreezingTest.agda | 13 -
.../GuardednessPreservingTypeConstructors.agda | 112 -
test/succeed/HereditarilySingletonRecord.agda | 47 -
test/succeed/Hurkens.agda | 47 -
test/succeed/ImplicitRecordFields.agda | 30 -
test/succeed/ImplicitsAndWhere.agda | 98 -
test/succeed/IndexInference.agda | 42 -
test/succeed/IndexOnBuiltin.agda | 18 -
.../InductiveAndCoinductiveConstructors.agda | 78 -
test/succeed/InferRecordTypes.agda | 36 -
test/succeed/InferrableFields.agda | 25 -
test/succeed/InfixRecordFields.agda | 35 -
test/succeed/InjectiveTypeConstructors.agda | 10 -
test/succeed/Injectivity.agda | 51 -
test/succeed/InstanceArguments.agda | 42 -
test/succeed/InstanceArgumentsBraces.agda | 9 -
test/succeed/InstanceArgumentsConstraints.agda | 24 -
...ontDiscardCandidateUponUnsolvedConstraints.agda | 28 -
test/succeed/InstanceArgumentsHidden.agda | 18 -
test/succeed/InstanceArgumentsSections.agda | 58 -
test/succeed/InstanceGuessesMeta.agda | 17 -
test/succeed/InstanceGuessesMeta2.agda | 33 -
.../IrrelevanceCaseStudyPartialFunctions.agda | 59 -
test/succeed/IrrelevantApplication.agda | 39 -
test/succeed/IrrelevantDataParameter.agda | 26 -
test/succeed/IrrelevantDeclaration.agda | 17 -
test/succeed/IrrelevantLambda.agda | 16 -
.../IrrelevantLambdasDoNotNeedDotsAlways.agda | 8 -
test/succeed/IrrelevantLet.agda | 11 -
test/succeed/IrrelevantLevel.agda | 47 -
test/succeed/IrrelevantProjections.agda | 13 -
test/succeed/IrrelevantRecordFields.agda | 44 -
test/succeed/IrrelevantWith.agda | 10 -
test/succeed/Issue100.agda | 8 -
test/succeed/Issue106.agda | 33 -
test/succeed/Issue107.agda | 16 -
test/succeed/Issue117.agda | 7 -
test/succeed/Issue121.agda | 21 -
test/succeed/Issue124.agda | 19 -
test/succeed/Issue133.agda | 30 -
test/succeed/Issue137.agda | 33 -
test/succeed/Issue138.agda | 9 -
test/succeed/Issue148.agda | 26 -
test/succeed/Issue151.agda | 33 -
test/succeed/Issue152.agda | 32 -
test/succeed/Issue153.agda | 31 -
test/succeed/Issue154.agda | 41 -
test/succeed/Issue155.agda | 15 -
test/succeed/Issue162.agda | 44 -
test/succeed/Issue165.agda | 17 -
test/succeed/Issue166.agda | 22 -
test/succeed/Issue168-irrelevant.agda | 20 -
test/succeed/Issue168.agda | 15 -
test/succeed/Issue168b.agda | 12 -
test/succeed/Issue175.agda | 24 -
test/succeed/Issue175b.agda | 44 -
test/succeed/Issue180.agda | 34 -
test/succeed/Issue199.agda | 11 -
test/succeed/Issue202.agda | 11 -
test/succeed/Issue203.agda | 28 -
test/succeed/Issue204.agda | 13 -
test/succeed/Issue204/Dependency.agda | 18 -
test/succeed/Issue209.agda | 34 -
test/succeed/Issue211.agda | 51 -
test/succeed/Issue213.agda | 12 -
test/succeed/Issue222.agda | 12 -
test/succeed/Issue224.agda | 21 -
test/succeed/Issue227.agda | 18 -
test/succeed/Issue229.agda | 16 -
test/succeed/Issue232.agda | 8 -
test/succeed/Issue233.agda | 10 -
test/succeed/Issue234.agda | 30 -
test/succeed/Issue237.agda | 21 -
test/succeed/Issue242.agda | 20 -
test/succeed/Issue245.agda | 36 -
test/succeed/Issue246.agda | 103 -
test/succeed/Issue248.agda | 23 -
test/succeed/Issue251.agda | 9 -
test/succeed/Issue252.agda | 24 -
test/succeed/Issue253.agda | 16 -
test/succeed/Issue258.agda | 9 -
test/succeed/Issue259.agda | 26 -
test/succeed/Issue259b.agda | 33 -
test/succeed/Issue259c.agda | 19 -
test/succeed/Issue26.agda | 21 -
test/succeed/Issue261.agda | 11 -
test/succeed/Issue262.agda | 6 -
test/succeed/Issue263.agda | 22 -
test/succeed/Issue263b.agda | 13 -
test/succeed/Issue268.agda | 79 -
test/succeed/Issue274.agda | 35 -
test/succeed/Issue276.agda | 32 -
test/succeed/Issue279.agda | 10 -
test/succeed/Issue282.agda | 31 -
test/succeed/Issue286.agda | 48 -
test/succeed/Issue291.agda | 45 -
test/succeed/Issue292-14.agda | 27 -
test/succeed/Issue292-16.agda | 32 -
test/succeed/Issue292-16b.agda | 32 -
test/succeed/Issue292-17.agda | 51 -
test/succeed/Issue292-19.agda | 37 -
test/succeed/Issue292-23.agda | 17 -
test/succeed/Issue292-27.agda | 23 -
test/succeed/Issue292.agda | 44 -
test/succeed/Issue296.agda | 15 -
test/succeed/Issue296.flags | 1 -
test/succeed/Issue298.agda | 20 -
test/succeed/Issue298b.agda | 15 -
test/succeed/Issue300.agda | 18 -
test/succeed/Issue307.agda | 24 -
test/succeed/Issue31.agda | 35 -
test/succeed/Issue311.agda | 35 -
test/succeed/Issue312.agda | 21 -
test/succeed/Issue313.agda | 14 -
test/succeed/Issue314.agda | 18 -
test/succeed/Issue323.agda | 12 -
test/succeed/Issue326.agda | 17 -
test/succeed/Issue326.flags | 1 -
test/succeed/Issue327.agda | 16 -
test/succeed/Issue330.agda | 19 -
test/succeed/Issue331.agda | 22 -
test/succeed/Issue333.agda | 21 -
test/succeed/Issue334.agda | 29 -
test/succeed/Issue335.agda | 8 -
test/succeed/Issue337.agda | 35 -
test/succeed/Issue34.agda | 18 -
test/succeed/Issue348.agda | 16 -
test/succeed/Issue351-5.agda | 11 -
test/succeed/Issue351.agda | 26 -
test/succeed/Issue353.agda | 21 -
test/succeed/Issue354.agda | 58 -
test/succeed/Issue361.agda | 21 -
test/succeed/Issue365.agda | 42 -
test/succeed/Issue366.agda | 29 -
test/succeed/Issue376.agda | 47 -
test/succeed/Issue383.agda | 37 -
test/succeed/Issue383b.agda | 30 -
test/succeed/Issue384.agda | 22 -
test/succeed/Issue387.agda | 16 -
test/succeed/Issue392.agda | 41 -
test/succeed/Issue395.agda | 6 -
test/succeed/Issue396.agda | 13 -
test/succeed/Issue396b.agda | 31 -
test/succeed/Issue408.agda | 55 -
test/succeed/Issue411.agda | 9 -
test/succeed/Issue414.agda | 13 -
test/succeed/Issue420.agda | 6 -
test/succeed/Issue421.agda | 37 -
test/succeed/Issue422.agda | 42 -
test/succeed/Issue423.agda | 79 -
test/succeed/Issue425.agda | 35 -
test/succeed/Issue427.agda | 13 -
test/succeed/Issue435.agda | 50 -
test/succeed/Issue438.agda | 23 -
test/succeed/Issue439.agda | 55 -
test/succeed/Issue44.agda | 37 -
test/succeed/Issue441.agda | 37 -
test/succeed/Issue442.agda | 17 -
test/succeed/Issue443.agda | 18 -
test/succeed/Issue447.agda | 16 -
test/succeed/Issue448.agda | 24 -
test/succeed/Issue450.agda | 41 -
test/succeed/Issue451.agda | 25 -
test/succeed/Issue455.agda | 44 -
test/succeed/Issue458.agda | 27 -
test/succeed/Issue458b.agda | 35 -
test/succeed/Issue462.agda | 41 -
test/succeed/Issue468.agda | 18 -
test/succeed/Issue469.agda | 38 -
test/succeed/Issue472.agda | 23 -
test/succeed/Issue473.agda | 74 -
test/succeed/Issue474.agda | 13 -
test/succeed/Issue475.agda | 23 -
test/succeed/Issue479.agda | 19 -
test/succeed/Issue480.agda | 57 -
test/succeed/Issue481.agda | 55 -
test/succeed/Issue481PonderBase.agda | 5 -
test/succeed/Issue481PonderImportMe.agda | 3 -
test/succeed/Issue481PonderMaster.agda | 7 -
test/succeed/Issue481Record.agda | 3 -
test/succeed/Issue482.agda | 21 -
test/succeed/Issue483.agda | 28 -
test/succeed/Issue483c.agda | 26 -
test/succeed/Issue486.agda | 14 -
test/succeed/Issue49.agda | 10 -
test/succeed/Issue498.agda | 69 -
test/succeed/Issue498b.agda | 36 -
test/succeed/Issue501.agda | 37 -
test/succeed/Issue502.agda | 7 -
test/succeed/Issue505.agda | 24 -
test/succeed/Issue509.agda | 50 -
test/succeed/Issue533.agda | 14 -
test/succeed/Issue550.agda | 23 -
test/succeed/Issue551b.agda | 20 -
test/succeed/Issue552.agda | 29 -
test/succeed/Issue553a.agda | 21 -
test/succeed/Issue553b.agda | 25 -
test/succeed/Issue553c.agda | 32 -
test/succeed/Issue557.agda | 25 -
test/succeed/Issue558.agda | 41 -
test/succeed/Issue558b.agda | 65 -
test/succeed/Issue558c.agda | 24 -
test/succeed/Issue561.agda | 20 -
test/succeed/Issue561.flags | 1 -
test/succeed/Issue566.agda | 29 -
test/succeed/Issue574.agda | 11 -
test/succeed/Issue578.agda | 16 -
test/succeed/Issue585-17.agda | 26 -
test/succeed/Issue586.agda | 6 -
test/succeed/Issue586.flags | 1 -
test/succeed/Issue593.agda | 52 -
test/succeed/Issue596.agda | 83 -
test/succeed/Issue597.agda | 52 -
test/succeed/Issue602-2.agda | 16 -
test/succeed/Issue602.agda | 47 -
test/succeed/Issue611.agda | 19 -
test/succeed/Issue616.agda | 13 -
test/succeed/Issue629.agda | 33 -
test/succeed/Issue629a.agda | 17 -
test/succeed/Issue655.agda | 52 -
test/succeed/Issue658.agda | 28 -
test/succeed/Issue661.agda | 46 -
test/succeed/Issue670a.agda | 15 -
test/succeed/Issue671.agda | 19 -
test/succeed/Issue674.agda | 25 -
test/succeed/Issue675.agda | 9 -
test/succeed/Issue678.agda | 46 -
test/succeed/Issue679.agda | 27 -
test/succeed/Issue680-NeutralLevels.agda | 28 -
test/succeed/Issue700.agda | 30 -
test/succeed/Issue701-c.agda | 32 -
test/succeed/Issue709.agda | 60 -
test/succeed/Issue728.agda | 5 -
test/succeed/Issue728.flags | 1 -
test/succeed/Issue735.agda | 72 -
test/succeed/Issue739.agda | 100 -
test/succeed/Issue747.agda | 34 -
test/succeed/Issue754.agda | 29 -
test/succeed/Issue81.agda | 21 -
test/succeed/Issue89.agda | 84 -
test/succeed/Issue97.lagda | 4 -
test/succeed/Issue97b.lagda | 13 -
test/succeed/JMEq.agda | 9 -
test/succeed/LaTeX.flags | 1 -
test/succeed/LaTeX.lagda | 69 -
test/succeed/Lambda.agda | 110 -
test/succeed/LateExpansionOfRecordMeta.agda | 32 -
test/succeed/LetLHS.agda | 7 -
test/succeed/LetPair.agda | 50 -
test/succeed/LevelConstraints.agda | 16 -
test/succeed/LevelUnification.agda | 18 -
test/succeed/LevelWithBug.agda | 68 -
test/succeed/LineEndings/Dos.agda | 3 -
test/succeed/LineEndings/Mac.agda | 1 -
test/succeed/LineEndings/Unix.agda | 3 -
test/succeed/LinearTemporalLogic.agda | 98 -
test/succeed/ListsWithIrrelevantProofs.agda | 39 -
test/succeed/LitDistinct.agda | 14 -
test/succeed/Literate.lagda | 21 -
test/succeed/LocalOpenImplicit.agda | 9 -
test/succeed/MagicWith.agda | 36 -
test/succeed/Makefile | 49 -
test/succeed/MatchIrrelevant.agda | 67 -
test/succeed/MixfixBinders.agda | 34 -
test/succeed/ModuleInstInLet.agda | 17 -
test/succeed/MultipleIdentifiersOneSignature.agda | 40 -
test/succeed/NameFirstIfHidden.agda | 16 -
test/succeed/NamedImplicit.agda | 36 -
test/succeed/NamedWhere.agda | 24 -
test/succeed/Nat.agda | 7 -
test/succeed/NestedInj.agda | 43 -
test/succeed/NoBlockOnLevel.agda | 35 -
test/succeed/NoTerminationCheck.agda | 66 -
test/succeed/NoUniverseCheck.agda | 21 -
test/succeed/NonvariantPolarity.agda | 81 -
test/succeed/OpBind.agda | 9 -
test/succeed/OpenModule.agda | 24 -
test/succeed/OpenModuleShortHand.agda | 21 -
test/succeed/OpenPublicTermination.agda | 20 -
test/succeed/Operators.agda | 42 -
test/succeed/OverloadedConInParamModule.agda | 16 -
test/succeed/OverloadedConstructors.agda | 25 -
test/succeed/Parity.agda | 39 -
test/succeed/PartialityMonad.agda | 34 -
.../PartiallyAppliedConstructorInIndex.agda | 15 -
test/succeed/PatternMatchingLambda.agda | 84 -
test/succeed/PatternSynonymImports.agda | 10 -
test/succeed/PatternSynonymImports2.agda | 10 -
test/succeed/PatternSynonyms.agda | 345 -
test/succeed/PiInSet.agda | 37 -
test/succeed/Point.agda | 29 -
test/succeed/PosFunction.agda | 24 -
test/succeed/Positivity.agda | 34 -
test/succeed/PostponedTypeChecking.agda | 29 -
test/succeed/PostponedUnification.agda | 31 -
test/succeed/Printf.agda | 106 -
test/succeed/ProjectingRecordMeta.agda | 26 -
.../ProjectionLikeAndConstructorHeaded.agda | 50 -
test/succeed/ProjectionLikeAndMatching.agda | 23 -
test/succeed/ProjectionLikeFunctions.agda | 30 -
test/succeed/ProjectionLikeRecursive.agda | 40 -
...ojectionsPreserveGuardednessTrivialExample.agda | 66 -
test/succeed/PruneLHS.agda | 17 -
test/succeed/PruningNonMillerPattern.agda | 94 -
test/succeed/QualifiedConstructors.agda | 32 -
test/succeed/QuoteTerm.agda | 28 -
test/succeed/RawFunctor.agda | 12 -
test/succeed/RecordConstructorPatternMatching.agda | 14 -
test/succeed/RecordConstructors.agda | 44 -
test/succeed/RecordInMutual.agda | 25 -
test/succeed/RecordInParModule.agda | 18 -
test/succeed/RecordPatternMatching.agda | 128 -
test/succeed/RecordUpdateSyntax.agda | 54 -
test/succeed/RecordsAndModules.agda | 26 -
test/succeed/ReducingConstructorsInWith.agda | 16 -
test/succeed/Reflection.agda | 133 -
.../succeed/ReifyConstructorParametersForWith.agda | 37 -
test/succeed/RelevanceSubtyping.agda | 10 -
.../Rewrite-with-doubly-indexed-equality.agda | 177 -
test/succeed/Rewrite.agda | 167 -
test/succeed/RewriteAndUniversePolymorphism.agda | 31 -
test/succeed/RewriteAndWhere.agda | 36 -
test/succeed/Rose.agda | 36 -
test/succeed/SafeFlagSafePragmas.agda | 3 -
test/succeed/SafeFlagSafePragmas.flags | 1 -
test/succeed/SameMeta.agda | 23 -
test/succeed/Shadow.agda | 9 -
test/succeed/ShadowedLetBoundVar.agda | 17 -
test/succeed/ShapeIrrelevantIndex.agda | 14 -
test/succeed/SizeSucMonotone.agda | 20 -
test/succeed/SizedBTree.agda | 34 -
test/succeed/SizedCoinductiveRecords.agda | 112 -
test/succeed/SizedTypesLeqInfty.agda | 19 -
test/succeed/SizedTypesMergeSort.agda | 47 -
test/succeed/SolveNeutralApplication.agda | 29 -
test/succeed/SplitOnDotPattern.agda | 18 -
test/succeed/Squash.agda | 18 -
test/succeed/StreamProcEat.agda | 69 -
test/succeed/SubTermAndProjections.agda | 36 -
test/succeed/Subset.agda | 8 -
test/succeed/SubtermTermination.agda | 48 -
test/succeed/TermSplicing.agda | 361 -
test/succeed/TerminationArgumentSwapping.agda | 53 -
test/succeed/TerminationListInsertionNaive.agda | 53 -
test/succeed/TerminationMixingTupledCurried.agda | 15 -
test/succeed/TerminationOnIrrelevantArgument.agda | 42 -
test/succeed/TerminationSubExpression.agda | 25 -
test/succeed/TerminationTupledAckermann.agda | 23 -
test/succeed/TerminationWithTwoConstructors.agda | 33 -
test/succeed/TestQuote.agda | 37 -
test/succeed/TopLevelImport.agda | 9 -
test/succeed/TransColist.agda | 62 -
.../TrustMe-with-doubly-indexed-equality.agda | 29 -
test/succeed/TrustMe.agda | 21 -
test/succeed/TypeInTypeAndUnivPoly.agda | 9 -
test/succeed/UncurryMeta.agda | 30 -
test/succeed/UnderscoresAsDataParam.agda | 5 -
test/succeed/UnicodeSetIndex.agda | 5 -
test/succeed/UnifyWithIrrelevantArgument.agda | 22 -
test/succeed/UniversePolymorphicIO.agda | 44 -
test/succeed/UniversePolymorphicIO.flags | 1 -
test/succeed/UniversePolymorphicIO.hs | 3 -
test/succeed/UniversePolymorphism.agda | 79 -
test/succeed/UnusedArgsInPositivity.agda | 63 -
test/succeed/UnusedNamedImplicits.agda | 36 -
test/succeed/Using.agda | 11 -
test/succeed/WErrorOverride.agda | 31 -
test/succeed/WErrorOverride.flags | 2 -
test/succeed/Whitespace.agda | 24 -
test/succeed/WhyWeNeedTypedLambda.agda | 30 -
test/succeed/WhyWeNeedUntypedLambda.agda | 26 -
test/succeed/WithInParModule.agda | 40 -
test/succeed/WithInWhere.agda | 25 -
test/succeed/WithoutK.agda | 70 -
test/succeed/builtin.agda | 163 -
test/succeed/builtinInModule.agda | 9 -
test/succeed/checkOutput | 13 -
test/succeed/list.agda | 13 -
test/succeed/local.agda | 23 -
test/succeed/optionsPragma.agda | 7 -
test/succeed/para.agda | 34 -
test/succeed/qsort.agda | 65 -
test/succeed/simple.agda | 146 -
3375 files changed, 37330 insertions(+), 157356 deletions(-)
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-haskell/agda.git
More information about the Pkg-haskell-commits
mailing list