2010 Archives by date

• Messages sorted by: [ thread ] [ subject ] [ author ]
• More info on this list...

Starting: Mon Jan 4 03:15:54 CEST 2010
Ending: Fri Dec 31 17:04:08 CEST 2010
Messages: 1061

• [Agda] (no subject)   KINOSHITA Yoshiki
• [Agda] agda error message   Martin Escardo
• [Agda] using inspect is tricky   Florent Balestrieri
• [Agda] agda error message   Andreas Abel
• [Agda] using inspect is tricky   Andreas Abel
• [Agda] agda error message   Martin Escardo
• [Agda] Agda with excluded middle is inconsistent   Chung Kil Hur
• [Agda] Agda with the excluded middle is inconsistent ?   Chung Kil Hur
• [Agda] conjectures in agda   Martin Escardo
• [Agda] Agda with the excluded middle is inconsistent ?   Dan Doel
• [Agda] conjectures in agda   Andrés Sicard-Ramírez
• [Agda] i-Society 2010: Call for Workshops!   David K Brown
• [Agda] conjectures in agda   Martin Escardo
• [Agda] Agda with the excluded middle is inconsistent ?   Chung Kil Hur
• [Agda] Agda with excluded middle is inconsistent   Thorsten Altenkirch
• [Agda] Agda with the excluded middle is inconsistent ?   Thorsten Altenkirch
• [Agda] Agda with the excluded middle is inconsistent ?   Dan Doel
• [Agda] Agda with excluded middle is inconsistent   Noam Zeilberger
• [Agda] Agda with excluded middle is inconsistent   Thorsten Altenkirch
• [Agda] Agda with the excluded middle is inconsistent ?   Thorsten Altenkirch
• [Agda] Agda with excluded middle is inconsistent   Noam Zeilberger
• [Agda] Agda with excluded middle is inconsistent   Dan Doel
• [Agda] Agda with excluded middle is inconsistent   Andreas Abel
• [Agda] Agda with excluded middle is inconsistent   Thorsten Altenkirch
• [Agda] Agda with excluded middle is inconsistent   Thorsten Altenkirch
• [Agda] Agda with excluded middle is inconsistent   Andreas Abel
• [Agda] Agda with the excluded middle is inconsistent ?   Benja Fallenstein
• [Agda] Agda with the excluded middle is inconsistent ?   Chung Kil Hur
• [Agda] Agda with excluded middle is inconsistent   Noam Zeilberger
• [Agda] Agda with the excluded middle is inconsistent ?   Thierry Coquand
• [Agda] Agda with the excluded middle is inconsistent ?   Thorsten Altenkirch
• [Agda] Agda with excluded middle is inconsistent   Nils Anders Danielsson
• [Agda] Agda with the excluded middle is inconsistent ?   Nils Anders Danielsson
• [Agda] Agda with excluded middle is inconsistent   Thorsten Altenkirch
• [Agda] Agda with excluded middle is inconsistent   David Wahlstedt
• [Agda] Agda with excluded middle is inconsistent   Noam Zeilberger
• [Agda] Agda with excluded middle is inconsistent   Thorsten Altenkirch
• [Agda] Bug?   Benja Fallenstein
• [Coq-Club] Re: [Agda] Agda with excluded middle is inconsistent   Benjamin Werner
• [Agda] Agda with excluded middle is inconsistent   Noam Zeilberger
• [Agda] Agda with the excluded middle is inconsistent ?   Noam Zeilberger
• [Agda] Agda with excluded middle is inconsistent   David Wahlstedt
• [Agda] Agda with excluded middle is inconsistent   Ulf Norell
• [Agda] Agda with excluded middle is inconsistent   Thorsten Altenkirch
• [Agda] FreeBSD and Agda   Jacula Modyun
• [Agda] FreeBSD and Agda   Jacula Modyun
• [Agda] Re: [Coq-Club] Agda with the excluded middle is inconsistent ?   roconnor at theorem.ca
• [Agda] FreeBSD and Agda   Nils Anders Danielsson
• [Agda] Agda with excluded middle is inconsistent   Nils Anders Danielsson
• [Agda] Re: [Coq-Club] Agda with the excluded middle is inconsistent ?   Chung Kil Hur
• [Agda] Agda with the excluded middle is inconsistent ?   herbelin
• [Agda] Re: [Coq-Club] Agda with the excluded middle is inconsistent ?   roconnor at theorem.ca
• [Agda] Agda with excluded middle is inconsistent   Martin Escardo
• [Agda] Agda with the excluded middle is inconsistent ?   Thierry Coquand
• [Agda] primes decidable   Ruben Henner Zilibowitz
• [Agda] primes decidable   Andreas Abel
• [Agda] primes decidable   Andreas Abel
• [Agda] Agda with the excluded middle is inconsistent ?   Andrew Pitts
• [Agda] primes decidable   Ruben Henner Zilibowitz
• [Agda] proving termination trouble again   Ruben Henner Zilibowitz
• [Agda] Agda with excluded middle is inconsistent   Anthony de Almeida Lopes
• [Agda] 4 PhD positions in Formalization of Mathematics in Type Theory   Thierry Coquand
• [Agda] proving termination trouble again   Andreas Abel
• [Agda] Agda with the excluded middle is inconsistent ?   Chung Kil Hur
• [Agda] Agda with the excluded middle is inconsistent ?   Andreas Abel
• [Agda] MiniAgda with the excluded middle is also inconsistent   Andreas Abel
• [Agda] Description Logics DL 2010 final call for papers   David Toman
• [Agda] Agda with the excluded middle is inconsistent ?   Andrew Pitts
• [Agda] Agda with the excluded middle is inconsistent ?   Thorsten Altenkirch
• [Agda] Optimised handling of records   Nils Anders Danielsson
• Sized Types [Re: [Agda] proving termination trouble again]   Robin Green
• [Agda] set levels in Algebra.Structure   Florent Balestrieri
• [Agda] set levels in Algebra.Structure   Nils Anders Danielsson
• [Agda] proving termination trouble again   Ruben Henner Zilibowitz
• Sized Types [Re: [Agda] proving termination trouble again]   Andreas Abel
• [Agda] Spring School in Generic and Indexed Programming   Jeremy.Gibbons at comlab.ox.ac.uk
• Sized Types [Re: [Agda] proving termination trouble again]   Ruben Henner Zilibowitz
• [Agda] HLDVT 2010: Call for Papers   Shireesh Verma
• Sized Types [Re: [Agda] proving termination trouble again]   Andreas Abel
• Sized Types [Re: [Agda] proving termination trouble again]   Andreas Abel
• Sized Types [Re: [Agda] proving termination trouble again]   Nils Anders Danielsson
• [Agda] Problem with coinduction and positivity checker   Simon Foster
• [Agda] Problem with coinduction and positivity checker   Andreas Abel
• [Agda] Problem with coinduction and positivity checker   Nils Anders Danielsson
• [Agda] PAR 2010: First CFP   Ana Bove
• [Agda] Problem with coinduction and positivity checker   Nils Anders Danielsson
• [Agda] wierd error   Ruben Henner Zilibowitz
• [Agda] wierd error   Ulf Norell
• [Agda] wierd error   Ruben Henner Zilibowitz
• [Agda] wierd error   Ulf Norell
• [Agda] wierd error   Ruben Henner Zilibowitz
• [Agda] wierd error   Ulf Norell
• [Agda] Pattern-matching, unfortunate effect on type   Florent Balestrieri
• [Agda] Pattern-matching, unfortunate effect on type   Andreas Abel
• [Agda] emacs agda mode bug (with expansion, coinduction)   Florent Balestrieri
• [Agda] emacs agda mode bug (with expansion, coinduction)   Nils Anders Danielsson
• [Agda] Pattern-matching, unfortunate effect on type   Nils Anders Danielsson
• [Agda] TFP 2010 - Call for Papers and Participation   TFP 2010
• [Agda] The sort of a datatype cannot depend on its indices   Chris Casinghino
• [Agda] The sort of a datatype cannot depend on its indices   Ulf Norell
• [Agda] Call for Papers: Haskell Symposium 2010   Jeremy.Gibbons at comlab.ox.ac.uk
• [Agda] AIM XI: Second Call for Participation   KINOSHITA Yoshiki
• [Agda] heterogeneous equality, library functions   Florent Balestrieri
• [Agda] Agda interface generation memory consumption   kahl at cas.mcmaster.ca
• [Agda] Agda interface generation memory consumption   Dan Doel
• [Agda] Agda interface generation memory consumption   Nils Anders Danielsson
• [Agda] Agda interface generation memory consumption   Nils Anders Danielsson
• [Agda] Agda interface generation memory consumption   Nils Anders Danielsson
• [Agda] Agda interface generation memory consumption   Dan Doel
• [Agda] minor bug with symbolic links in include path   Florent Balestrieri
• [Agda] Agda interface generation memory consumption   Nils Anders Danielsson
• [Agda] Agda interface generation memory consumption   Nils Anders Danielsson
• [Agda] minor bug with symbolic links in include path   Nils Anders Danielsson
• [Agda] Agda interface generation memory consumption   kahl at cas.mcmaster.ca
• [Agda] WGP 2010 - Call for papers   Bruno Oliveira
• [Agda] Agda interface generation memory consumption   Nils Anders Danielsson
• [Agda] Agda interface generation memory consumption   Darin Morrison
• [Agda] Agda interface generation memory consumption   kahl at cas.mcmaster.ca
• [Agda] Pattern-matching operation order   Pierre Boutillier
• [Agda] Agda interface generation memory consumption   kahl at cas.mcmaster.ca
• [Agda] WGP 2010 Call for Papers   Bruno Oliveira
• [Agda] ​Call for Papers: LICE-2010!   m.smith at liceducation.org
• [Agda] Agda interface generation memory consumption   Nils Anders Danielsson
• [Agda] Pattern-matching operation order   Nils Anders Danielsson
• [Agda] Pattern-matching operation order   Andreas Abel
• [Agda] Pattern-matching operation order   Ulf Norell
• [Agda] HLDVT 2010 Final Call for Papers   Shireesh Verma
• [Agda] Respects2 in IsPreorder is derivable   kahl at cas.mcmaster.ca
• [Agda] DEPENDENTLY TYPED PROGRAMMING 2010 (CFP)   Thorsten Altenkirch
• [Agda] DEPENDENTLY TYPED PROGRAMMING 2010 (CFP)   Thorsten Altenkirch
• [Agda] Respects2 in IsPreorder is derivable   Nils Anders Danielsson
• [Agda] Pattern-matching operation order   Andreas Abel
• [Agda] Pattern-matching operation order   Ulf Norell
• [Agda] Pattern-matching operation order   Dan Licata
• [Agda] VIM syntax highlighting for Agda   Petr Pudlak
• [Agda] VIM syntax highlighting for Agda   Anthony de Almeida Lopes
• [Agda] VIM syntax highlighting for Agda   Nicolas Pouillard
• [Agda] VIM syntax highlighting for Agda   Nils Anders Danielsson
• [Agda] VIM syntax highlighting for Agda   Anthony
• [Agda] VIM syntax highlighting for Agda   Ulf Norell
• [Agda] VIM syntax highlighting for Agda   Anthony
• [Agda] Pattern-matching operation order   Andreas Abel
• [Agda] VIM syntax highlighting for Agda   Petr Pudlak
• [Agda] ICFP 2010: Second call for papers   Wouter Swierstra
• [Agda] VIM syntax highlighting for Agda   Anthony
• [Agda] Decidable partial orders   Peter Berry
• [Agda] Re: Decidable partial orders   Peter Berry
• [Agda] PLMMS 2010 Call for Papers   Lucas Dixon
• [Agda] MSFP: Call for Papers   Venanzio Capretta
• [Agda] Absurd catch all pattern   Andreas Abel
• [Agda] Absurd catch all pattern   Nils Anders Danielsson
• [Agda] Absurd catch all pattern   Ulf Norell
• [Agda] HLDVT 2010 Paper submission deadline extended to March 14!!!   Shireesh Verma
• [Agda] PAR'10 at FLOC'10: 2nd CFP   Ana Bove
• [Agda] reflective access to definitional equality   Dan Licata
• [Agda] Re: reflective access to definitional equality   Stefan Monnier
• [Agda] LFMTP 2010 at FLoC: Call for Papers   Marino Miculan
• [Agda] Automatheo 2010 at FLoC: Call for Papers, Talks, and System Demonstrations   Lucas Dixon
• [Agda] reflective access to definitional equality   Wouter Swierstra
• [Agda] TFP 2010 - 3rd CFP: Submit papers by April 9, REGISTRATION IS OPEN   TFP 2010
• [Agda] LFMTP 2010 at FLoC: Call for Papers (CORRECT DATES)   Marino Miculan
• [Agda] PLMMS 2010: Last Call for Papers   Lucas Dixon
• [Agda] ring solver   Ruben Henner Zilibowitz
• [Agda] ring solver   Nils Anders Danielsson
• [Agda] ring solver   Ruben Henner Zilibowitz
• [Agda] Final Call for Papers: LICE-2010!   m.smith at liceducation.org
• [Agda] ring solver   Nils Anders Danielsson
• [Agda] ring solver   Ruben Henner Zilibowitz
• [Agda] equality reasoning and contradictory type indices   Chris Casinghino
• [Agda] equality reasoning and contradictory type indices   Nils Anders Danielsson
• [Agda] equality reasoning and contradictory type indices   Chris Casinghino
• [Agda] Emacs special character input   Carl
• [Agda] Emacs special character input   Nils Anders Danielsson
• [Agda] CFPapers: 22nd Symposium on Implementation and Applications of Functional Languages (IFL 2010)   jur
• [Agda] pattern matching bug?   Chris Casinghino
• [Agda] pattern matching bug?   Nils Anders Danielsson
• [Agda] HLDVT 2010 Paper Submission Deadline Extended to March 24!   Shireesh Verma
• [Agda] More aggressive type reconstruction?   Andreas Abel
• Sized Types [Re: [Agda] proving termination trouble again]   Ruben Henner Zilibowitz
• Sized Types [Re: [Agda] proving termination trouble again]   Andreas Abel
• [Agda] yet another grinding reload   Conor McBride
• Sized Types [Re: [Agda] proving termination trouble again]   Ruben Henner Zilibowitz
• [Agda] ICFP 2010: Final Call for Papers   Wouter Swierstra
• Sized Types [Re: [Agda] proving termination trouble again]   Andreas Abel
• [Agda] PAR'10 at FLOC'10: -- Final CFP   Ana Bove
• [Agda] LFMTP 2010 at FLoC: Final Call for Papers   Marino Miculan
• [Agda] yet another grinding reload   Ulf Norell
• [Agda] 64-bit agda   James Chapman
• [Agda] 64-bit agda   Nils Anders Danielsson
• [Agda] 64-bit agda   Manuel M T Chakravarty
• [Agda] DEPENDENTLY TYPED PROGRAMMING 2010 (CFP)   Thorsten Altenkirch
• [Agda] yet another grinding reload   Conor McBride
• [Agda] 64-bit agda   Sean Leather
• [Agda] ICFP 2010 deadline   Wouter Swierstra
• [Agda] PLMMS 2010: Call for Demos   Lucas Dixon
• [Agda] 64-bit agda   James Chapman
• [Agda] 64-bit agda   Guillaume Allais
• [Agda] 64-bit agda   Nils Anders Danielsson
• [Agda] 64-bit agda   James Chapman
• [Agda] MSFP: last call for papers   Venanzio Capretta
• [Agda] TFP 2010 - Final Call: Submission deadline one week away, April 9   TFP 2010
• [Agda] 64-bit agda   Nils Anders Danielsson
• [Agda] LFMTP 2010 at FLoC: extended deadline   Marino Miculan
• [Agda] yet another grinding reload   Nils Anders Danielsson
• [Agda] Guardedness-preserving type constructors   Nils Anders Danielsson
• [Agda] Guardedness-preserving type constructors   Thorsten Altenkirch
• [Agda] 2nd CFP: 6th ACM SIGPLAN Workshop on Generic Programming   Shin-Cheng Mu
• [Agda] Call for Contributions - Haskell Communities and Activities Report, May 2010 edition   Janis Voigtländer
• [Agda] Agda with GHC-6.10.4, continued...   kahl at cas.mcmaster.ca
• [Agda] Agda error reporting   kahl at cas.mcmaster.ca
• [Agda] Agda error reporting   Ulf Norell
• [Agda] Agda error reporting   Nils Anders Danielsson
• [Agda] Agda error reporting   kahl at cas.mcmaster.ca
• [Agda] Are .agdai files portable?   kahl at cas.mcmaster.ca
• [Agda] Are .agdai files portable?   Nils Anders Danielsson
• [Agda] Are .agdai files portable?   Iain Lane
• [Agda] ​Call for Workshops and Tutorials: ICITST-2010!   g.akmayeva at icitst.org
• [Agda] Are .agdai files portable?   Nicolas Pouillard
• [Agda] Agda error reporting   Nils Anders Danielsson
• [Agda] Re: Agda with GHC-6.10.4, continued...   Nils Anders Danielsson
• [Agda] Are .agdai files portable?   Nils Anders Danielsson
• [Agda] Re: Agda with GHC-6.10.4, continued...   kahl at cas.mcmaster.ca
• [Agda] Are .agdai files portable?   Nils Anders Danielsson
• [Agda] PhD and postdoc position in China/UK   Thomas ANBERREE
• [Agda] Agda assessed exercises   Sam Staton
• [Agda] PAR-10 call for participation and informal presentations   Ana Bove
• [Agda] newbie: installation problem   Randy Pollack
• [Agda] newbie: installation problem   Guillaume Allais
• [Agda] newbie: installation problem   Iain Lane
• [Agda] newbie: installation problem   Nils Anders Danielsson
• [Agda] implicit parameters and 'with'   Florent Balestrieri
• [Agda] implicit parameters and 'with'   Ulf Norell
• [Agda] DEPENDENTLY TYPED PROGRAMMING 2010 (CFP)   Thorsten Altenkirch
• [Agda] Agda's standard lib does not typecheck any more   Dirk Ullrich
• [Agda] instance functor Sigma   Dan Licata
• [Agda] Automatheo 2010 at FLoC: Final Call for Papers, Talks, and System Demonstrations   Lucas Dixon
• [Agda] Dependencies for compiling agda, principal question   David Wahlstedt
• [Agda] Dependencies for compiling agda, principal question   James McKinna
• [Agda] Dependencies for compiling agda, principal question   Martin Escardo
• [Agda] Dependencies for compiling agda, principal question   Darin Morrison
• [Agda] Dependencies for compiling agda, principal question   Darin Morrison
• [Agda] Agda's standard lib does not typecheck any more   Nils Anders Danielsson
• [Agda] instance functor Sigma   Pierre-Evariste Dagand
• [Agda] Dependencies for compiling agda, principal question   David Wahlstedt
• [Agda] instance functor Sigma   Dan Licata
• [Agda] Dependencies for compiling agda, principal question   Darin Morrison
• [Agda] Dependencies for compiling agda, principal question   Nils Anders Danielsson
• [Agda] Dependencies for compiling agda, principal question   Nils Anders Danielsson
• [Agda] Dependencies for compiling agda, principal question   Iain Lane
• [Agda] Dependencies for compiling agda, principal question   Nils Anders Danielsson
• [Agda] Dependencies for compiling agda, principal question   David Wahlstedt
• [Agda] Some comments on agda performance   Alan Jeffrey
• [Agda] Re: Dependencies for compiling agda, principal question   Stefan Monnier
• [Agda] Re: Dependencies for compiling agda, principal question   Ulf Norell
• [Agda] Re: Dependencies for compiling agda, principal question   James Chapman
• [Agda] Some comments on agda performance   Nils Anders Danielsson
• [Agda] install darcs version?   Martin Escardo
• [Agda] install darcs version?   Randy Pollack
• [Agda] install darcs version?   Nils Anders Danielsson
• [Agda] Induction-recursion, indexing and universes.   Dan Doel
• [Agda] Re: Induction-recursion, indexing and universes.   Dan Doel
• [Agda] Observational equality model   Jean-Philippe Bernardy
• [Agda] Observational equality model   Conor McBride
• [Agda] Observational equality model   Jean-Philippe Bernardy
• [Agda] 2nd CfP: 20th WADT - deadline April, 30th   Till Mossakowski
• [Agda] install darcs version?   Randy Pollack
• [Agda] install darcs version?   Nicolas Pouillard
• [Agda] Debugging Agda's syntaxes   David Haguenauer
• [Agda] Debugging Agda's syntaxes   Ulf Norell
• [Agda] install darcs version?   Nils Anders Danielsson
• [Agda] Call for Participation: FLoC Workshop on Modules and Libraries for Proof Assistants   Florian Rabe
• [Agda] Debugging Agda's syntaxes   David Haguenauer
• [Agda] What's the type of Set?   Chris Casinghino
• [Agda] What's the type of Set?   Ulf Norell
• [Agda] What's the type of Set?   Nils Anders Danielsson
• [Agda] What's the type of Set?   Chris Casinghino
• [Agda] REMINDER: Haskell Communities and Activities Report   Janis Voigtländer
• [Agda] CfP: 20th WADT - deadline extended to May, 10th   Till Mossakowski
• [Agda] Agda web framework   Larrytheliquid
• [Agda] WGP 2010 Second Call for Papers   Bruno Oliveira
• [Agda] some brown for your nerves   Conor McBride
• [Agda] some brown for your nerves   James Chapman
• [Agda] some brown for your nerves   Conor McBride
• [Agda] some brown for your nerves   Nils Anders Danielsson
• [Agda] some brown for your nerves   Andreas Abel
• [Agda] Agda web framework   Jeremy Shaw
• [Agda] PAR'10: Call for Participation   Ana Bove
• [Agda] agda-mode on mac os   Rypacek, Ondrej
• [Agda] DTP 2010: call for participation   Thorsten Altenkirch
• [Agda] agda-mode on mac os   Nils Anders Danielsson
• [Agda] agda-mode on mac os   Rypacek, Ondrej
• [Agda] agda-mode on mac os   Nils Anders Danielsson
• [Agda] agda-mode on mac os   Rypacek, Ondrej
• [Agda] Lightweight free theorems   Jean-Philippe Bernardy
• [Agda] Lightweight free theorems   Jean-Philippe Bernardy
• [Agda] LFMTP 2010 at FLoC: Call for participation   Marino Miculan
• [Agda] Deadline for HLDVT early registration closes May 17   Shireesh Verma
• [Agda] 2nd CFP: SSV'10 @ USENIX OSDI 2010   Gerwin Klein
• [Agda] Debugging Agda's syntaxes   David Haguenauer
• [Agda] Debugging Agda's syntaxes   Ulf Norell
• [Agda] Automatheo 2010 at FLoC: Call for Participation and Registration   Lucas Dixon
• [Agda] Agda Implementors' Meeting XII   Nils Anders Danielsson
• [Agda] Talk on integrating automated and interactive theorem proving in Agda   Anton Setzer
• [Agda] Call for Participation: 20th WADT, July 1-4, 2010   Till Mossakowski
• [Agda] 2nd CFPapers: 22nd Symposium on Implementation and Applications of Functional Languages (IFL 2010)   jur
• [Agda] Agda's mixfix parser   Stefan Monnier
• [Agda] Agda's mixfix parser   Nils Anders Danielsson
• [Agda] ANNOUNCE: Haskell Communities and Activities Report (18th ed., May 2010)   Janis Voigtländer
• [Agda] Heterogeneous Vectors   Simon Foster
• [Agda] mu-nu in Agda   Thorsten Altenkirch
• [Agda] Heterogeneous Vectors   Thorsten Altenkirch
• [Agda] mu-nu in Agda   Andreas Abel
• [Agda] Types Meeting 2010   Aleksy Schubert
• [Agda] weird behavior with large records   Chris Casinghino
• [Agda] weird behavior with large records   Andrés Sicard-Ramírez
• [Agda] weird behavior with large records   Chris Casinghino
• [Agda] weird behavior with large records   Nils Anders Danielsson
• [Agda] running out of memory in formalization of category theory   Dan Licata
• [Agda] running out of memory in formalization of category theory   Thorsten Altenkirch
• [Agda] running out of memory in formalization of category theory   Ulf Norell
• [Agda] running out of memory in formalization of category theory   Conor McBride
• [Agda] running out of memory in formalization of category theory   Nils Anders Danielsson
• [Agda] running out of memory in formalization of category theory   Anton Setzer
• [Agda] ICFP Programming Contest   Wouter Swierstra
• [Agda] running out of memory in formalization of category theory   Nils Anders Danielsson
• [Agda] Final Call for Papers: Haskell Symposium 2010   Jeremy.Gibbons at comlab.ox.ac.uk
• [Agda] running out of memory in formalization of category theory   Nicolas Pouillard
• [Agda] Workshop on Generic Programming (WGP) 2010 Final Call for Papers   Bruno Oliveira
• [Agda] running out of memory in formalization of category theory   Nils Anders Danielsson
• [Agda] running out of memory in formalization of category theory   kahl at cas.mcmaster.ca
• [Agda] running out of memory in formalization of category theory   Nicolas Pouillard
• [Agda] running out of memory in formalization of category theory   Nils Anders Danielsson
• [Agda] running out of memory in formalization of category theory   Nils Anders Danielsson
• [Agda] running out of memory in formalization of category theory   Dan Licata
• [Agda] running out of memory in formalization of category theory   Dan Licata
• [Agda] running out of memory in formalization of category theory   Nils Anders Danielsson
• [Agda] CFP - PSC Track @ SAC 2011   Emiliano Tramontana
• [Agda] agda-mode stopped working   Thorsten Altenkirch
• [Agda] agda-mode stopped working   Andrés Sicard-Ramírez
• [Agda] agda-mode stopped working   Nils Anders Danielsson
• [Agda] agda-mode stopped working   Thorsten Altenkirch
• [Agda] agda-mode stopped working   Nils Anders Danielsson
• [Agda] agda-mode stopped working   Thorsten Altenkirch
• [Agda] agda-mode stopped working   Nils Anders Danielsson
• [Agda] Self-containing inductive-recursive definitions   Dan Doel
• [Agda] Self-containing inductive-recursive definitions   Nils Anders Danielsson
• [Agda] Call for contributed talks (Trusted Extensions of ITPs)   Matt Kaufmann
• [Agda] Equivalence axiom => extensionality   Thorsten Altenkirch
• [Agda] Equivalence axiom => extensionality   Dan Licata
• [Agda] formalization of category theory   Vag Vagoff
• [Agda] formalization of category theory   kahl at cas.mcmaster.ca
• [Agda] Fully-funded PhD in programming languages at Oxford   Jeremy.Gibbons at comlab.ox.ac.uk
• [Agda] Self-containing inductive-recursive definitions   Thorsten Altenkirch
• [Agda] formalization of category theory   Thorsten Altenkirch
• [Agda] formalization of category theory   Thorsten Altenkirch
• [Agda] Self-containing inductive-recursive definitions   Dan Doel
• [Agda] Self-containing inductive-recursive definitions   Thorsten Altenkirch
• [Agda] Equivalence axiom => extensionality   Thorsten Altenkirch
• [Agda] Self-containing inductive-recursive definitions   Dan Licata
• [Agda] Equivalence axiom => extensionality   Dan Licata
• [Agda] PLMMS-2010 call for participation   Lucas Dixon
• [Agda] ​ICITST-2010: Paper Submission Deadline Extended to June 30   r.ho at icitst.org
• [Agda] Equivalence axiom => extensionality   Thorsten Altenkirch
• [Agda] Equivalence axiom => extensionality   Dan Licata
• [Agda] Equivalence axiom => extensionality   Thorsten Altenkirch
• [Agda] Equivalence axiom => extensionality   Thorsten Altenkirch
• [Agda] Equivalence axiom => extensionality   Bas Spitters
• [Agda] Equivalence axiom => extensionality   Dan Licata
• [Agda] Fully funded Master of Research studentship on algebraic modelling of test data   Anton Setzer
• [Agda] Equivalence axiom => extensionality   Thorsten Altenkirch
• [Agda] Equivalence axiom => extensionality   Peter LeFanu Lumsdaine
• [Agda] Equivalence axiom => extensionality   Thorsten Altenkirch
• [Agda] Modeling reflective languages   Alan Jeffrey
• [Agda] Floatpoint priorities (to wish list)   Vag Vagoff
• [Agda] Re: Floatpoint priorities (to wish list)   Vag Vagoff
• [Agda] Floatpoint priorities (to wish list)   Nils Anders Danielsson
• [Agda] Re: Floatpoint priorities (to wish list)   Serguey Zefirov
• [Agda] Re: Floatpoint priorities (to wish list)   Nils Anders Danielsson
• [Agda] Floatpoint priorities (to wish list)   Vag Vagoff
• [Agda] Floatpoint priorities (to wish list)   Nils Anders Danielsson
• [Agda] Equivalence axiom => extensionality   Dan Doel
• [Agda] Equivalence axiom => extensionality   Peter LeFanu Lumsdaine
• [Agda] 3nd CFPapers en 1st CFPart: 22nd Symposium on Implementation and Application of Functional Languages.   jur
• [Agda] TLDI 2011 Call For Papers   Stephanie Weirich
• [Agda] "with" notation?   Randy Pollack
• [Agda] "with" notation?   Pierre-Evariste Dagand
• [Agda] "with" notation?   Randy Pollack
• [Agda] "with" notation?   Pierre-Evariste Dagand
• [Agda] How to formalize 'there exists a set' phrase?   Vag Vagoff
• [Agda] How to formalize 'there exists a set' phrase?   Nils Anders Danielsson
• [Agda] "with" notation?   Nils Anders Danielsson
• [Agda] How to formalize 'there exists a set' phrase?   Vag Vagoff
• [Agda] How to formalize 'there exists a set' phrase?   Benja Fallenstein
• [Agda] How to formalize 'there exists a set' phrase?   Rypacek, Ondrej
• [Agda] How to formalize 'there exists a set' phrase?   Andreas Abel
• [Agda] How to formalize 'there exists a set' phrase?   Benja Fallenstein
• [Agda] How to set up fixities for record parameters?   Vag Vagoff
• [Agda] How to set up fixities for record parameters?   Vag
• [Agda] How to set up fixities for record parameters?   Vag
• [Agda] How to set up fixities for record parameters?   Vag
• [Agda] How to set up fixities for record parameters?   Vag
• [Agda] How to formalize 'there exists a set' phrase?   Rypacek, Ondrej
• [Agda] How to formalize 'there exists a set' phrase?   Dan Doel
• [Agda] How to formalize 'there exists a set' phrase?   Dan Doel
• [Agda] Problems installing the standard library   Robert Rothenberg
• [Agda] "Problem encountered. The *ghci* buffer perhaps can explain why"   Robert Rothenberg
• [Agda] How to formalize 'there exists a set' phrase?   Thorsten Altenkirch
• [Agda] How to formalize 'there exists a set' phrase?   Ondrej Rypacek
• [Agda] "Problem encountered. The *ghci* buffer perhaps can explain why"   Nils Anders Danielsson
• [Agda] Problems installing the standard library   Nils Anders Danielsson
• [Agda] why it can no be parsed ?   Leonardo Rodriguez
• [Agda] lhs2TeX for agda   Ondrej Rypacek
• [Agda] why it can no be parsed ?   gallais at EnsL
• [Agda] Re: lhs2TeX for agda   Ondrej Rypacek
• [Agda] why it can no be parsed ?   Chris Casinghino
• [Agda] why it can no be parsed ?   Vag Vagoff
• [Agda] Re: lhs2TeX for agda   Neil Sculthorpe
• [Agda] Re: lhs2TeX for agda   Ondrej Rypacek
• [Agda] Re: lhs2TeX for agda   Neil Sculthorpe
• [Agda] Re: lhs2TeX for agda   Chantal Keller
• [Agda] Re: lhs2TeX for agda   Darin Morrison
• [Agda] Equivalence axiom => extensionality   Dan Doel
• [Agda] Fwd: Lhs2Tex and unicode   Jean-Philippe Bernardy
• [Agda] Mutual clause   Leonardo Rodriguez
• [Agda] Mutual clause   Leonardo Rodriguez
• [Agda] Equivalence axiom => extensionality   Andreas Abel
• [Agda] Fwd: Lhs2Tex and unicode   Ondrej Rypacek
• [Agda] Agda Implementors' Meeting XII   Nils Anders Danielsson
• [Agda] Equivalence axiom => extensionality   Dan Doel
• [Agda] Equivalence axiom => extensionality   Dan Licata
• [Agda] Surprising type error in implementing decreasing lists   Alan Jeffrey
• [Agda] Surprising type error in implementing decreasing lists   Conor McBride
• [Agda] Surprising type error in implementing decreasing lists   Nils Anders Danielsson
• [Agda] Surprising type error in implementing decreasing lists   Nils Anders Danielsson
• [Agda] Surprising type error in implementing decreasing lists   Nils Anders Danielsson
• [Agda] Surprising type error in implementing decreasing lists   Ulf Norell
• [Agda] Surprising type error in implementing decreasing lists   Alan Jeffrey
• [Agda] Equivalence axiom => extensionality   Dan Doel
• [Agda] ICFP 2010: Call for participation   Wouter Swierstra
• [Agda] ICFP 2010: Call for participation   James Chapman
• [Agda] MSFP call for participation   Venanzio Capretta
• [Agda] Agda mysteriously hangs   Josh Ko
• [Agda] Agda mysteriously hangs   Andreas Abel
• [Agda] Agda mysteriously hangs   Josh Ko
• [Agda] RingSolver, normalisation   Christoph HERRMANN
• [Agda] RingSolver, normalisation   Andreas Abel
• [Agda] RingSolver, normalisation   Christoph HERRMANN
• [Agda] Commutativity problems in RingSolver   Christoph HERRMANN
• [Agda] Re: Commutativity problems in RingSolver   Christoph HERRMANN
• [Agda] Ringsolver seems ok, but how to get NF?   Christoph HERRMANN
• [Agda] Ringsolver seems ok, but how to get NF?   Nils Anders Danielsson
• [Agda] Commutativity problems in RingSolver   Nils Anders Danielsson
• [Agda] Ringsolver seems ok, but how to get NF?   Christoph HERRMANN
• [Agda] Reminder: Agda Implementors' Meeting XII   Nils Anders Danielsson
• [Agda] Ringsolver seems ok, but how to get NF?   Nils Anders Danielsson
• [Agda] Ringsolver seems ok, but how to get NF?   Christoph HERRMANN
• [Agda] ICFP '10: Final call for participation   Wouter Swierstra
• [Agda] Ringsolver seems ok, but how to get NF?   Nils Anders Danielsson
• [Agda] Ringsolver seems ok, but how to get NF?   Christoph HERRMANN
• [Agda] Ringsolver seems ok, but how to get NF?   Nils Anders Danielsson
• [Agda] Speeding up Agda   Christoph HERRMANN
• [Agda] Speeding up Agda   Nils Anders Danielsson
• [Agda] PSC track at SAC: deadline extension   Tramontana Emiliano
• [Agda] Haskell 2010 Call for Participation   Jeremy.Gibbons at comlab.ox.ac.uk
• [Agda] MSFP - early registration: 30 August   Venanzio Capretta
• [Agda] sequencing 3 IO operations   Jeremy Shaw
• [Agda] sequencing 3 IO operations   Nils Anders Danielsson
• [Agda] AIM XII: Preliminary program   Nils Anders Danielsson
• [Agda] sequencing 3 IO operations   Alan Jeffrey
• [Agda] Types'10 - Call for Participation   Aleksy Schubert
• [Agda] patch: documentation updates in the parser   Jean-Philippe Bernardy
• [Agda] TLDI 2011: 2nd Call For Papers   Stephanie Weirich
• [Agda] heterogeneous equality   Andrés Sicard-Ramírez
• [Agda] heterogeneous equality   Nils Anders Danielsson
• [Agda] heterogeneous equality   Andrés Sicard-Ramírez
• [Agda] ​Call for Papers: WorldCIS-2011   Paul Kelly
• [Agda] heterogeneous equality   Nils Anders Danielsson
• [Agda] Mixfix binders: first patch   Jean-Philippe Bernardy
• [Agda] Mixfix binders: first patch   Dan Doel
• [Agda] Mixfix binders: first patch   Ulf Norell
• [Agda] Proofs for enumerated types   Gregory Crosswhite
• [Agda] Proofs for enumerated types   Nils Anders Danielsson
• [Agda] Mixfix binders: first patch   Jean-Philippe Bernardy
• [Agda] Mixfix binders: first patch   Andreas Abel
• [Agda] Mixfix binders: first patch   Nils Anders Danielsson
• [Agda] Mixfix binders: first patch   Nils Anders Danielsson
• [Agda] Call for Paper: TLCA'11, 1-3 June 2011, Novi Sad   Luca Paolini
• [Agda] Call for Paper: TLCA'11, 1-3 June 2011, Novi Sad   Luca Paolini
• [Agda] Mixfix binders: first patch   Andreas Abel
• [Agda] Mixfix binders: first patch   Nils Anders Danielsson
• [Agda] Mixfix binders: first patch   Andreas Abel
• [Agda] Mixfix binders: first patch   Nils Anders Danielsson
• [Agda] Mixfix binders: first patch   Ulf Norell
• [Agda] Refectoring Builtins   Simon Foster
• [Agda] Refectoring Builtins   Ulf Norell
• [Agda] Mixfix binders: first patch   Jean-Philippe Bernardy
• [Agda] Mixfix binders: first patch   Nils Anders Danielsson
• [Agda] Mixfix binders: first patch   Ulf Norell
• [Agda] Refectoring Builtins   Simon Foster
• [Agda] Mixfix binders: first patch   Jean-Philippe Bernardy
• [Agda] Proofs for enumerated types   Gregory Crosswhite
• [Agda] Refectoring Builtins   Ulf Norell
• [Agda] Proposed minor additions to standard library   Gregory Crosswhite
• [Agda] Feedback requested on automated decision module   Gregory Crosswhite
• [Agda] PLPV 2010 Call for Papers   Wouter Swierstra
• [Agda] Feedback requested on automated decision module   Nils Anders Danielsson
• [Agda] Proposed minor additions to standard library   Nils Anders Danielsson
• [Agda] Proposed minor additions to standard library   Jason Reich
• [Agda] Refectoring Builtins   Simon Foster
• [Agda] Proposed minor additions to standard library   Nils Anders Danielsson
• [Agda] Refectoring Builtins   Ulf Norell
• [Agda] Proposed minor additions to standard library   Dan Licata
• [Agda] Mixfix binders: first patch   Andreas Abel
• [Agda] Re: Feedback requested on automated decision module   Samuel Gélineau
• [Agda] Feedback requested on automated decision module   Samuel Gélineau
• [Agda] Proposed minor additions to standard library   Dan Doel
• [Agda] Proposed minor additions to standard library   Nils Anders Danielsson
• [Agda] Testing new Haskell functions   Simon Foster
• [Agda] trustMe and make my coercion go   Benja Fallenstein
• [Agda] trustMe and make my coercion go   Andreas Abel
• [Agda] Proofs for enumerated types   Daniel Brown
• [Agda] trustMe and make my coercion go   Benja Fallenstein
• [Agda] trustMe and make my coercion go   Andreas Abel
• [Agda] trustMe and make my coercion go   Benja Fallenstein
• [Agda] Coming soon: Agda 2.2.8   Nils Anders Danielsson
• [Agda] Re: [Coq-Club] Re: Universe Polymorphism   Dan Doel
• [Agda] Agda FFI bindings   Alan Jeffrey
• [Agda] Re: [Coq-Club] Re: Universe Polymorphism   Jean-Philippe Bernardy
• [Agda] Re: [Coq-Club] Re: Universe Polymorphism   Dan Doel
• [Agda] Records and irrelevant fields   Andreas Abel
• [Agda] Agda FFI bindings   Nils Anders Danielsson
• [Agda] Records and irrelevant fields   Dan Doel
• [Agda] Records and irrelevant fields   Andreas Abel
• [Agda] Agda FFI bindings   Alan Jeffrey
• [Agda] Agda github organization?   Alan Jeffrey
• [Agda] Records and irrelevant fields   Dan Doel
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] Records and irrelevant fields   wren ng thornton
• [Agda] Records and irrelevant fields   Dan Doel
• [Agda] Records and irrelevant fields   wren ng thornton
• [Agda] Records and irrelevant fields   Dan Doel
• [Agda] A question on records   David Leduc
• [Agda] A question on records   Jean-Philippe Bernardy
• [Agda] Re: [Coq-Club] Re: Universe Polymorphism   Jean-Philippe Bernardy
• [Agda] RDP 2011 -- Call For Workshop Proposals   Luca Paolini
• [Agda] Re: [Coq-Club] Re: Universe Polymorphism   Dan Doel
• [Agda] Again, a question on records   David Leduc
• [Agda] Again, a question on records   Dan Doel
• [Agda] Again, a question on records   David Leduc
• [Agda] Again, a question on records   David Leduc
• [Agda] Again, a question on records   Benja Fallenstein
• [Agda] Again, a question on records   Dan Doel
• [Agda] Again, a question on records   David Leduc
• [Agda] Again, a question on records   Benja Fallenstein
• [Agda] Again, a question on records   David Leduc
• [Agda] Re: [Coq-Club] Re: Universe Polymorphism   Jean-Philippe Bernardy
• [Agda] Post Doctoral Position in Formalization of Mathematics   Thierry Coquand
• [Agda] not strictly positive?! I don't believe it!   David Leduc
• [Agda] Pie in the sky (was: Again, a question on records)   Samuel Gélineau
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] not strictly positive?! I don't believe it!   Andreas Abel
• [Agda] not strictly positive?! I don't believe it!   Andreas Abel
• Pie in the sky Re: [Agda] Again, a question on records   Andreas Abel
• Pie in the sky Re: [Agda] Again, a question on records   Benja Fallenstein
• [Agda] Pie in the sky (was: Again, a question on records)   Benja Fallenstein
• [Agda] Records and irrelevant fields   Andreas Abel
• [Agda] Pie in the sky (was: Again, a question on records)   Patrik Jansson
• [Agda] Records and irrelevant fields   Dan Doel
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] Pie in the sky   Samuel Gélineau
• [Agda] Pie in the sky   Benja Fallenstein
• [Agda] Records and irrelevant fields   Andreas Abel
• [Agda] Pie in the sky   Andreas Abel
• [Agda] Records and irrelevant fields   Dan Doel
• [Agda] a bug in the type checker?   David Leduc
• [Agda] Pie in the sky   Benja Fallenstein
• [Agda] a bug in the type checker?   Ulf Norell
• [Agda] Pie in the sky   Benja Fallenstein
• [Agda] Pie in the sky   Samuel Gélineau
• [Agda] Re: Agda github organization?   Alan Jeffrey
• [Agda] Again, a question on records   Nils Anders Danielsson
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] Pie in the sky   Benja Fallenstein
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] Re: Agda FFI bindings   Brandon Moore
• [Agda] Re: Agda FFI bindings   Peter Hancock
• [Agda] Re: Agda FFI bindings   kahl at cas.mcmaster.ca
• [Agda] Pie in the sky   Samuel Gélineau
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] Pie in the sky   Benja Fallenstein
• [Agda] Re: Agda FFI bindings   Benja Fallenstein
• [Agda] Records and irrelevant fields   Dan Doel
• [Agda] Pie in the sky   Dan Licata
• [Agda] IO, semi-closed handles, and problems with extensional equality   Alan Jeffrey
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] Records and irrelevant fields   wren ng thornton
• [Agda] IO, semi-closed handles, and problems with extensional equality   Lennart Augustsson
• [Agda] IO, semi-closed handles, and problems with extensional equality   Christoph Herrmann
• [Agda] 3 newbie's questions, sorry!   David Leduc
• [Agda] IO, semi-closed handles, and problems with extensional equality   Alan Jeffrey
• [Agda] IO, semi-closed handles, and problems with extensional equality   Alan Jeffrey
• [Agda] A question on Setoid in the standard library   David Leduc
• [Agda] Re: A question on Setoid in the standard library   David Leduc
• [Agda] 3 newbie's questions, sorry!   gallais at EnsL
• [Agda] Agda FFI bindings   Anton Setzer
• [Agda] IO, semi-closed handles, and problems with extensional equality   Anton Setzer
• [Agda] IO, semi-closed handles, and problems with extensional equality   Alan Jeffrey
• [Agda] IO, semi-closed handles, and problems with extensional equality   Anton Setzer
• [Agda] IO, semi-closed handles, and problems with extensional equality   Alan Jeffrey
• Introducing the finite-prover library (was: [Agda] Feedback requested on automated decision module)   Samuel Gélineau
• [Agda] Records and irrelevant fields   Andreas Abel
• [Agda] IO, semi-closed handles, and problems with extensional equality   Anton Setzer
• [Agda] IO, semi-closed handles, and problems with extensional equality   Anton Setzer
• [Agda] Records and irrelevant fields   Dan Doel
• [Agda] IO, semi-closed handles, and problems with extensional equality   Alan Jeffrey
• [Agda] Records and irrelevant fields   Andreas Abel
• [Agda] 3 newbie's questions, sorry!   Andreas Abel
• [Agda] Trying to use irrelevant arguments to get a nicer equality for algebraic structures   Andrea Vezzosi
• [Agda] Records and irrelevant fields   Dan Doel
• [Agda] ​CICE-2011: Call for Papers!   Margaret Smith
• [Agda] IO, semi-closed handles, and problems with extensional equality   Peter Hancock
• [Agda] Pie in the sky   Samuel Gélineau
• [Agda] Trying to use irrelevant arguments to get a nicer equality for algebraic structures   Andreas Abel
• [Agda] Pie in the sky   Benja Fallenstein
• [Agda] Pie in the sky   Benja Fallenstein
• [Agda] IO, semi-closed handles, and problems with extensional equality   Alan Jeffrey
• [Agda] 3 newbie's questions, sorry!   Nils Anders Danielsson
• [Agda] Re: A question on Setoid in the standard library   Nils Anders Danielsson
• [Agda] Re: Agda github organization?   Nils Anders Danielsson
• [Agda] Re: Agda FFI bindings   Nils Anders Danielsson
• [Agda] Re: Agda FFI bindings   Nils Anders Danielsson
• [Agda] Re: Agda FFI bindings   Nils Anders Danielsson
• [Agda] Pie in the sky   Bas Spitters
• [Agda] Postdoc vacancies in OUCL Information Systems Group   Ian Horrocks
• [Agda] Proving equality of pairs   David Leduc
• [Agda] Makefile   David Leduc
• [Agda] Proving equality of pairs   Andreas Abel
• [Agda] Makefile   Andreas Abel
• [Agda] Irrelevant record fields   Andreas Abel
• [Agda] Pie in the sky   Samuel Gélineau
• [Agda] Problem with the termination checker   David Leduc
• [Agda] Makefile   David Leduc
• [Agda] Pie in the sky   Alan Jeffrey
• [Agda] Problem with the termination checker   Andreas Abel
• [Agda] Problem with the termination checker   David Leduc
• [Agda] Proving equality of pairs   David Leduc
• [Agda] Pie in the sky   Thorsten Altenkirch
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] Pie in the sky   Samuel Gélineau
• [Agda] Makefile   Samuel Gélineau
• [Agda] Trying to use irrelevant arguments to get a nicer equality for algebraic structures   Andrea Vezzosi
• [Agda] Trying to use irrelevant arguments to get a nicer equality for algebraic structures   Andreas Abel
• [Agda] Proving equality of pairs   Andreas Abel
• [Agda] Re: Irrelevant record fields   Andrea Vezzosi
• [Agda] Proving equality of pairs   Brandon Moore
• [Agda] Pie in the sky   Alan Jeffrey
• [Agda] Pie in the sky   Alan Jeffrey
• [Agda] Pie in the sky   Alan Jeffrey
• [Agda] Proving equality of pairs   Nils Anders Danielsson
• [Agda] Problem with the termination checker   Nils Anders Danielsson
• [Agda] Makefile   Nils Anders Danielsson
• [Agda] Pie in the sky   Samuel Gélineau
• [Agda] Pie in the sky   Benja Fallenstein
• [Agda] Pie in the sky   Andreas Abel
• [Agda] Proving equality of pairs   Andreas Abel
• [Agda] Pie in the sky   Andreas Abel
• [Agda] Again, a question on records   David Leduc
• Agda in Agda [Was: [Agda] Pie in the sky]   Samuel Gélineau
• Agda in Agda [Was: [Agda] Pie in the sky]   Benja Fallenstein
• [Agda] order inside a mutual block is relevant?   David Leduc
• Agda in Agda [Was: [Agda] Pie in the sky]   Benja Fallenstein
• [Agda] Again, a question on records   Andreas Abel
• [Agda] order inside a mutual block is relevant?   Andreas Abel
• Agda in Agda [Was: [Agda] Pie in the sky]   Samuel Gélineau
• Agda in Agda [Was: [Agda] Pie in the sky]   Nils Anders Danielsson
• [Agda] Pie in the sky   Nils Anders Danielsson
• [Agda] Again, a question on records   David Leduc
• [Agda] Pie in the sky   Alan Jeffrey
• Agda in Agda [Was: [Agda] Pie in the sky]   Benja Fallenstein
• [Agda] Pie in the sky   Alan Jeffrey
• Agda in Agda [Was: [Agda] Pie in the sky]   Benja Fallenstein
• [Agda] Level ω   David Leduc
• [Agda] Level ω   Dan Doel
• Re: [Agda] Level ω   David Leduc
• Re: [Agda] Level ω   Andreas Abel
• Re: [Agda] Level ω   David Leduc
• [Agda] dependent extensionality   David Leduc
• Re: [Agda] Level ω   Andreas Abel
• [Agda] Pie in the sky   Alan Jeffrey
• [Agda] Agda type inference oddity on functions   Alan Jeffrey
• [Agda] Agda type inference oddity on functions   Thorsten Altenkirch
• [Agda] Agda type inference oddity on functions   Alan Jeffrey
• [Agda] Agda type inference oddity on functions   Nils Anders Danielsson
• [Agda] Agda type inference oddity on functions   Alan Jeffrey
• [Agda] ANNOUNCE: Agda 2.2.8   Nils Anders Danielsson
• [Agda] ANNOUNCE: Standard library version 0.4   Nils Anders Danielsson
• [Agda] Agda type inference oddity on functions   Thorsten Altenkirch
• [Agda] rewrite vs. with   David Leduc
• [Agda] rewrite vs. with   Jean-Philippe Bernardy
• [Agda] dependent extensionality   Thorsten Altenkirch
• [Agda] Agda type inference oddity on functions   Alan Jeffrey
• [Agda] Positivity checker, record vs data   Florent Balestrieri
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Andreas Abel
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Ulf Norell
• [Agda] Positivity checker, record vs data   Ulf Norell
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Alan Jeffrey
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Andreas Abel
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Alan Jeffrey
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Andreas Abel
• [Agda] dependent extensionality   James Chapman
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Alan Jeffrey
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Andreas Abel
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Alan Jeffrey
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Nils Anders Danielsson
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Thorsten Altenkirch
• [Agda] dependent extensionality   Thorsten Altenkirch
• [Agda] dependent extensionality   James Chapman
• [Agda] Bug in the strictly positivity check   Florent Balestrieri
• [Agda] rewrite vs. with   David Leduc
• [Agda] dependent extensionality   Thorsten Altenkirch
• [Agda] rewrite vs. with   Jean-Philippe Bernardy
• [Agda] Bug in the strictly positivity check   Florent
• [Agda] rewrite vs. with   David Leduc
• [Agda] rewrite vs. with   Jean-Philippe Bernardy
• [Agda] Bug in the strictly positivity check   Dan Doel
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Conor McBride
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Andreas Abel
• [Agda] dependent extensionality   James Chapman
• [Agda] dependent extensionality   James Chapman
• [Agda] dependent extensionality   Conor McBride
• [Agda] dependent extensionality   Vladimir Voevodsky
• [Agda] dependent extensionality   Thorsten Altenkirch
• [Agda] vertical bars | in my goal   David Leduc
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Nils Anders Danielsson
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]   Conor McBride
• [Agda] Record definition being in scope during type checking can cause Agda to hang   Iain Lane
• [Agda] First cut of semantics-preserving IO bindings   Alan Jeffrey
• [Agda] Re: vertical bars | in my goal   David Leduc
• [Agda] Re: vertical bars | in my goal   Ulf Norell
• [Agda] This must be a type checking bug, right?   David Leduc
• [Agda] Does Agda2 have fast arrays?   Permjacov Evgeniy
• [Agda] This must be a type checking bug, right?   Andreas Abel
• [Agda] Does Agda2 have fast arrays?   Andreas Abel
• [Agda] Does Agda2 have fast arrays?   Thorsten Altenkirch
• [Agda] Does Agda2 have fast arrays?   Don Stewart
• [Agda] Does Agda2 have fast arrays?   Nils Anders Danielsson
• [Agda] Does Agda2 have fast arrays?   Daniel Peebles
• [Agda] Does Agda2 have fast arrays?   Don Stewart
• [Agda] Does Agda2 have fast arrays?   Don Stewart
• [Agda] Does Agda2 have fast arrays?   Andreas Abel
• [Agda] Does Agda2 have fast arrays?   Conor McBride
• Compilation [Re: [Agda] Does Agda2 have fast arrays?]   Andreas Abel
• [Agda] Does Agda2 have fast arrays?   Don Stewart
• [Agda] This must be a type checking bug, right?   Jean-Philippe Bernardy
• [Agda] Does Agda2 have fast arrays?   Dan Licata
• [Agda] Does Agda2 have fast arrays?   Conor McBride
• [Agda] Does Agda2 have fast arrays?   Don Stewart
• [Agda] Does Agda2 have fast arrays?   Andreas Abel
• [Agda] Record definition being in scope during type checking can cause Agda to hang   Nils Anders Danielsson
• [Agda] Does Agda2 have fast arrays?   Don Stewart
• [Agda] Coinductive families   Dan Doel
• [Agda] Coinductive families   Andreas Abel
• [Agda] Coinductive families   Dan Doel
• [Agda] Coinductive families   Andreas Abel
• [Agda] Type error?? But I'm sure it's well-typed!   David Leduc
• [Agda] Coinductive families   Nils Anders Danielsson
• [Agda] TLDI 2011: Final CALL FOR PAPERS   Stephanie Weirich
• [Agda] Type error?? But I'm sure it's well-typed!   Andreas Abel
• [Agda] Type error?? But I'm sure it's well-typed!   David Leduc
• [Agda] Does Agda2 have fast arrays?   Alan Jeffrey
• [Agda] Does Agda2 have fast arrays?   Don Stewart
• [Agda] Does Agda2 have fast arrays?   Daniel Peebles
• [Agda] Does Agda2 have fast arrays?   Alan Jeffrey
• [Agda] Does Agda2 have fast arrays?   Daniel Peebles
• [Agda] Coinductive families   Thorsten Altenkirch
• [Agda] Re: Does Agda2 have fast arrays?   Permjacov Evgeniy
• [Agda] Type error?? But I'm sure it's well-typed!   Nils Anders Danielsson
• [Agda] Re: Agda FFI bindings   Nils Anders Danielsson
• [Agda] IO, semi-closed handles, and problems with extensional equality   Nils Anders Danielsson
• [Agda] Testing new Haskell functions   Nils Anders Danielsson
• [Agda] Coinductive families   Andreas Abel
• [Agda] Does Agda2 have fast arrays?   Alan Jeffrey
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] IO, semi-closed handles, and problems with extensional equality   Alan Jeffrey
• [Agda] Re: Agda FFI bindings   Nils Anders Danielsson
• [Agda] Does Agda2 have fast arrays?   Don Stewart
• [Agda] Coinductive families   Dan Doel
• [Agda] What is coinduction?   Gregory Crosswhite
• [Agda] Coinductive families   Anton Setzer
• [Agda] What is coinduction?   David Leduc
• [Agda] What is coinduction?   David Leduc
• [Agda] Coinductive families   Anton Setzer
• [Agda] Coinductive families   Dan Doel
• [Agda] What is coinduction?   wren ng thornton
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] Re: Agda FFI bindings   Daniel Peebles
• [Agda] What is coinduction?   Peter Berry
• [Agda] Does Agda2 have fast arrays?   Alan Jeffrey
• [Agda] Does Agda2 have fast arrays?   Brandon Moore
• [Agda] What is coinduction?   Gregory Crosswhite
• [Agda] What is coinduction?   Jean-Philippe Bernardy
• [Agda] Re: Agda FFI bindings   Nicolas Pouillard
• [Agda] Coinductive families   Thorsten Altenkirch
• [Agda] Coinductive families   Thorsten Altenkirch
• [Agda] Coinductive families   Dan Doel
• [Agda] Coinductive families   Dan Doel
• [Agda] Coinductive families   Thorsten Altenkirch
• [Agda] Coinductive families   Thorsten Altenkirch
• [Agda] Coinductive families   Andreas Abel
• [Agda] Coinductive families   Andreas Abel
• [Agda] Coinductive families   Andreas Abel
• [Agda] Coinductive families   Nils Anders Danielsson
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] Type error?? But I'm sure it's well-typed!   David Leduc
• [Agda] Does Agda2 have fast arrays?   Alan Jeffrey
• [Agda] Coinductive families   Dan Licata
• [Agda] Type error?? But I'm sure it's well-typed!   Nils Anders Danielsson
• [Agda] Coinductive families   Nils Anders Danielsson
• [Agda] Coinductive families   Nils Anders Danielsson
• [Agda] Does Agda2 have fast arrays?   Alan Jeffrey
• [Agda] Type theory at IAS   Vladimir Voevodsky
• [Agda] Coinductive families   Anton Setzer
• [Agda] Coinductive families   Nicolas Pouillard
• [Agda] Coinductive families   Dan Doel
• [Agda] IO, semi-closed handles, and problems with extensional equality   Alan Jeffrey
• [Agda] IO, semi-closed handles, and problems with extensional equality   wren ng thornton
• [Agda] Coinductive families   Nicolas Pouillard
• [Agda] Re: Agda FFI bindings   Nicolas Pouillard
• [Agda] Coinductive families   Andreas Abel
• [Agda] Coinductive families   Andreas Abel
• [Agda] Coinductive families   Nils Anders Danielsson
• [Agda] Coinductive families   Nils Anders Danielsson
• [Agda] Coinductive families   Thorsten Altenkirch
• [Agda] Coinductive families   Nils Anders Danielsson
• [Agda] Re: Agda FFI bindings   Alan Jeffrey
• [Agda] IO, semi-closed handles, and problems with extensional equality   Alan Jeffrey
• [Agda] Coinductive families   Nicolas Pouillard
• [Agda] RTA CFP 2011   Masahiko Sakai (RTA publicity chair)
• [Agda] PhD place at the FP lab, Nottingham   Thorsten Altenkirch
• [Agda] PhD place at the FP lab, Nottingham   Thorsten Altenkirch
• [Agda] Coinductive families   Andreas Abel
• [Agda] Coinductive families   Nicolas Pouillard
• [Agda] Coinductive families   Thorsten Altenkirch
• [Agda] CFP: Special issue on DEPENDENTLY TYPED PROGRAMMING 2010   Thorsten Altenkirch
• [Agda] Does Agda2 have fast arrays?   Gregory Crosswhite
• [Agda] Call for Contributions - Haskell Communities and Activities Report, November 2010 edition   Janis Voigtländer
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Oscar Finnsson
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Thorsten Altenkirch
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Thorsten Altenkirch
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Samuel Gélineau
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Dan Doel
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Jean-Philippe Bernardy
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Ulf Norell
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Andreas Abel
• Language Design considerations [Re: [Agda] Newbie questions after reading Dependently Typed Programming in Agda]   Andreas Abel
• Language Design considerations [Re: [Agda] Newbie questions after reading Dependently Typed Programming in Agda]   Jean-Philippe Bernardy
• Language Design considerations [Re: [Agda] Newbie questions after reading Dependently Typed Programming in Agda]   Ulf Norell
• Language Design considerations [Re: [Agda] Newbie questions after reading Dependently Typed Programming in Agda]   Andreas Abel
• Language Design considerations [Re: [Agda] Newbie questions after reading Dependently Typed Programming in Agda]   Andreas Abel
• Language Design considerations [Re: [Agda] Newbie questions after reading Dependently Typed Programming in Agda]   Nils Anders Danielsson
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Nils Anders Danielsson
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Nils Anders Danielsson
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Oscar Finnsson
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Jean-Philippe Bernardy
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Andreas Abel
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Thorsten Altenkirch
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Nicolas Pouillard
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Thorsten Altenkirch
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Conor McBride
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Nicolas Pouillard
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Thorsten Altenkirch
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Thorsten Altenkirch
• [Agda] main, IO, agda -c, Nat and Float   Oscar Finnsson
• [Agda] main, IO, agda -c, Nat and Float   Nils Anders Danielsson
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Nils Anders Danielsson
• [Agda] main, IO, agda -c, Nat and Float   Alan Jeffrey
• [Agda] main, IO, agda -c, Nat and Float   Andreas Abel
• [Agda] Newbie questions after reading Dependently Typed Programming in Agda   Nicolas Pouillard
• [Agda] main, IO, agda -c, Nat and Float   Edwin Brady
• [Agda] Agda IO with session types   Alan Jeffrey
• [Agda] Agda IO with session types   Gregory Crosswhite
• [Agda] Agda IO with session types   Alan Jeffrey
• [Agda] Feature request: array primitives   Permjacov Evgeniy
• [Agda] Agda IO with session types   Peter Hancock
• [Agda] Feature request: array primitives   Nils Anders Danielsson
• [Agda] Agda IO with session types   Alan Jeffrey
• [Agda] Raw natural numbers   Alan Jeffrey
• [Agda] Raw natural numbers   Ulf Norell
• [Agda] PostDoc and PhD Positions at Yale University   Zhong Shao
• [Agda] Raw natural numbers   Alan Jeffrey
• [Agda] Raw natural numbers   Alan Jeffrey
• [Agda] ICFP 2011: Call for Workshop Proposals   Wouter Swierstra
• [Agda] Re: Agda IO with session types   Alan Jeffrey
• [Agda] 2012-2013 special program at IAS   Vladimir Voevodsky
• [Agda] REMINDER: Haskell Communities and Activities Report, November 2010 edition   Janis Voigtländer
• [Agda] Re: Agda IO with session types   Nils Anders Danielsson
• [Agda] Re: Agda IO with session types   Alan Jeffrey
• [Agda] Compiler works ahead   Andreas Abel
• [Agda] Compiler works ahead   Daniel Peebles
• [Agda] Compiler works ahead   Andreas Abel
• [Agda] Compiler works ahead   Daniel Peebles
• [Agda] Compiler works ahead   Daniel Peebles
• [Agda] Compiler works ahead   Jean-Philippe Bernardy
• [Agda] Compiler works ahead   Alan Jeffrey
• [Agda] Compiler works ahead   Nils Anders Danielsson
• [Agda] lhs2tex and with   Dan Licata
• [Agda] lhs2tex and with   kahl at cas.mcmaster.ca
• [Agda] lhs2tex and with   Dan Licata
• [Agda] lhs2tex and with   Nils Anders Danielsson
• [Agda] Raw natural numbers   Ulf Norell
• [Agda] Raw natural numbers   Alan Jeffrey
• [Agda] Raw natural numbers   Alan Jeffrey
• [Agda] Incompatible interface files?   Dirk Ullrich
• [Agda] Patch for compilation with GHC-7   kahl at cas.mcmaster.ca
• [Agda] Incompatible interface files?   Nils Anders Danielsson
• [Agda] Patch for compilation with GHC-7   Nils Anders Danielsson
• [Agda] Patch for compilation with GHC-7   kahl at cas.mcmaster.ca
• [Agda] Incompatible interface files?   Dirk Ullrich
• [Agda] Absurd pattern in implicit argument of a lambda abstraction   Florent Balestrieri
• [Agda] Absurd pattern in implicit argument of a lambda abstraction   Dan Doel
• [Agda] Patch for compilation with GHC-7   Nils Anders Danielsson
• [Agda] Strictly positivity of indexed families   Florent Balestrieri
• [Agda] Strictly positivity of indexed families   Dan Licata
• [Agda] Patch for compilation with GHC-7   Nils Anders Danielsson
• [Agda] Strictly positivity of indexed families   Anton Setzer
• [Agda] Patch for compilation with GHC-7   kahl at cas.mcmaster.ca
• [Agda] Patch for compilation with GHC-7   Andreas Abel
• [Agda] Patch for compilation with GHC-7   Nils Anders Danielsson
• [Agda] Patch for compilation with GHC-7   kahl at cas.mcmaster.ca
• [Agda] Patch for compilation with GHC-7   Nils Anders Danielsson
• [Agda] Patch for compilation with GHC-7   kahl at cas.mcmaster.ca
• [Agda] Patch for compilation with GHC-7   Nils Anders Danielsson
• [Agda] ANNOUNCE: Haskell Communities and Activities Report (19th ed., November 2010)   Janis Voigtländer
• [Agda] Raw natural numbers   Ulf Norell
• [Agda] Raw natural numbers   Alan Jeffrey
• [Agda] Weird behaviour with record normalisation   Simon Foster
• [Agda] Weird behaviour with record normalisation   Andreas Abel
• [Agda] Weird behaviour with record normalisation   Simon Foster
• [Agda] Weird behaviour with record normalisation   Andreas Abel
• [Agda] Weird behaviour with record normalisation   Andreas Abel
• [Agda] Weird behaviour with record normalisation   Simon Foster
• [Agda] Ill shaped metavariable?   Ondrej Rypacek
• [Agda] Ill shaped metavariable?   Larrytheliquid
• [Agda] Failed type checking of standard lib after removed eta-contraction of function bodies in `Def.hs'   Dirk Ullrich
• [Agda] mutual recursion   Dan Licata
• [Agda] Ill shaped metavariable?   Ondrej Rypacek
• [Agda] Ill shaped metavariable?   Nicolas Pouillard
• [Agda] mutual recursion   Thorsten Altenkirch
• [Agda] Failed type checking of standard lib after removed eta-contraction of function bodies in `Def.hs'   Andreas Abel
• [Agda] mutual recursion   Nils Anders Danielsson
• [Agda] New Agda dependencies cause conflict   Andreas Abel
• [Agda] New Agda dependencies cause conflict   Andreas Abel
• [Agda] New Agda dependencies cause conflict   James Chapman
• [Agda] New Agda dependencies cause conflict   Andreas Abel
• [Agda] Failed type checking of standard lib after removed eta-contraction of function bodies in `Def.hs'   Andreas Abel
• [Agda] New Agda dependencies cause conflict   Dirk Ullrich
• Eta-reduction for records buggy [Re: [Agda] Weird behaviour with record normalisation]   Andreas Abel
• [Agda] Failed type checking of standard lib after removed eta-contraction of function bodies in `Def.hs'   Dirk Ullrich
• [Agda] New Agda dependencies cause conflict   Nils Anders Danielsson
• [Agda] New Agda dependencies cause conflict   Andrés Sicard-Ramírez
• [Agda] Difference between "(f o g) x = .." and "(f o g) = \ x -> .."   Edsko de Vries
• [Agda] Difference between "(f o g) x = .." and "(f o g) = \ x -> .."   Nils Anders Danielsson
• [Agda] A type for positive type functors?   Dominique Devriese
• [Agda] A type for positive type functors?   Dan Licata
• [Agda] A type for positive type functors?   Andreas Abel
• [Agda] A type for positive type functors?   Dominique Devriese
• [Agda] A type for positive type functors?   Dominique Devriese
• [Agda] A type for positive type functors?   Nicolas Pouillard
• First-class positivity and injectivity [Re: [Agda] A type for positive type functors?]   Andreas Abel
• [Agda] A type for positive type functors?   Thorsten Altenkirch
• [Agda] A type for positive type functors?   Dominique Devriese
• [Agda] A type for positive type functors?   Thorsten Altenkirch
• [Agda] A type for positive type functors?   Andreas Abel
• [Agda] A type for positive type functors?   Thorsten Altenkirch
• [Agda] A type for positive type functors?   Dominique Devriese
• [Agda] A type for positive type functors?   Sam Staton
• [Agda] A type for positive type functors?   Nils Anders Danielsson
• [Agda] importing syntax declarations   Benedict Kavanagh
• [Agda] importing syntax declarations   Jean-Philippe Bernardy
• [Agda] importing syntax declarations   Nils Anders Danielsson
• [Agda] How to activate DEBUG in Data.HashTable?   Wolfram Kahl
• [Agda] Agda darcs patches for additional reporting   Wolfram Kahl
• [Agda] Re: How to activate DEBUG in Data.HashTable?   Simon Marlow
• [Agda] .agdai serialisation runs into segfault in Data.HashTable   Wolfram Kahl
• [Agda] Pointwise function equality   Dominique Devriese
• [Agda] Pointwise function equality   Thorsten Altenkirch
• [Agda] quotient types   Ondrej Rypacek
• [Agda] quotient types   Nils Anders Danielsson
• [Agda] .agdai serialisation runs into segfault in Data.HashTable   Nils Anders Danielsson
• [Agda] TLDI 2011 Call for participation   Stephanie Weirich
• [Agda] Two best practice questions   Edsko de Vries
• [Agda] Two best practice questions   Andreas Abel
• [Agda] Two best practice questions   Conor McBride
• [Agda] importing syntax declarations   Nicolas Pouillard
• [Agda] RTA 2011: 2nd call for papers   Masahiko Sakai (RTA publicity chair)
• [Agda] Container isomorphism?   Edsko de Vries
• [Agda] Container isomorphism?   Andreas Abel
• [Agda] Container isomorphism?   Edsko de Vries
• [Agda] Container isomorphism?   Edsko de Vries
• [Agda] Container isomorphism?   Thorsten Altenkirch
• [Agda] quotient types   Ondrej Rypacek
• [Agda] quotient types   Nils Anders Danielsson
• [Agda] CFP ICFP 2011   Wouter Swierstra
• [Agda] Incompatibilities affecting ``Fresh Look''   kahl at cas.mcmaster.ca
• [Agda] Incompatibilities affecting ``Fresh Look''   Nils Anders Danielsson
• [Agda] Incompatibilities affecting ``Fresh Look''   Nicolas Pouillard
• [Agda] Epic compiler backend.   Daniel Gustafsson
• [Agda] Epic compiler backend.   Andreas Abel
• [Agda] Epic compiler backend.   Olle Fredriksson
• [Agda] Epic compiler backend.   Edwin Brady
• [Agda] Fwd: Re: epic-0.1.5 installation problem   Andreas Abel
• [Agda] Epic compiler backend.   Nils Anders Danielsson
• [Agda] Incompatibilities affecting ``Fresh Look''   kahl at cas.mcmaster.ca
• [Agda] Incompatibilities affecting ``Fresh Look''   Julian Beaumont
• [Agda] Incompatibilities affecting ``Fresh Look''   kahl at cas.mcmaster.ca
• [Agda] Incompatibilities affecting ``Fresh Look''   Julian Beaumont
• [Agda] 1st CFP Trends in Functional Pogramming 2011   Ricardo Peña
• [Agda] Incompatibilities affecting ``Fresh Look''   kahl at cas.mcmaster.ca
• [Agda] Incompatibilities affecting ``Fresh Look''   Andreas Abel
• [Agda] Incompatibilities affecting ``Fresh Look''   Alan Jeffrey
• [Agda] Incompatibilities affecting ``Fresh Look''   Nils Anders Danielsson
• [Agda] Incompatibilities affecting ``Fresh Look''   kahl at cas.mcmaster.ca
• [Agda] Size of propositional equality?   Alan Jeffrey
• [Agda] Size of propositional equality?   Nils Anders Danielsson
• [Agda] Size of propositional equality?   Alan Jeffrey
• [Agda] Raw natural numbers   Alan Jeffrey
• [Agda] Size of propositional equality?   Nils Anders Danielsson
• [Agda] Size of propositional equality?   Andreas Abel
• [Agda] Size of propositional equality?   Thorsten Altenkirch
• [Agda] Epic compiler backend.   Andrés Sicard-Ramírez
• [Agda] Size of propositional equality?   Peter Dybjer
• [Agda] Size of propositional equality?   Andreas Abel
• [Agda] size-based termination   Ondrej Rypacek
• [Agda] size-based termination   Andreas Abel
• [Agda] size-based termination   Conor McBride
• [Agda] size-based termination   Andreas Abel
• [Agda] Post-Doc at Carnegie Mellon   Steve Awodey
• [Agda] size-based termination   Ondrej Rypacek
• [Agda] size-based termination   Andreas Abel
• [Agda] size-based termination   Ondrej Rypacek
• [Agda] TLCA 2011 --- Last Call for Papers   Luca Paolini
• [Agda] Size of propositional equality?   Dan Licata
• [Agda] Records & dependent pattern matching   gallais at EnsL.org
• [Agda] Not implemented: coinductive constructor in the scope of a let-bound variable   Thorsten Altenkirch
• [Agda] Records & dependent pattern matching   Andreas Abel
• [Agda] Not implemented: coinductive constructor in the scope of a let-bound variable   Andreas Abel
• [Agda] Records & dependent pattern matching   gallais at EnsL.org
• [Agda] generative thunk?   Conor McBride
• [Agda] Records & dependent pattern matching   Andreas Abel
• [Agda] generative thunk?   Andreas Abel
• [Agda] generative thunk?   Conor McBride
• [Agda] generative thunk?   Conor McBride
• [Agda] generative thunk?   Thorsten Altenkirch
• [Agda] generative thunk?   Nils Anders Danielsson
• [Agda] Not implemented: coinductive constructor in the scope of a let-bound variable   Nils Anders Danielsson
• [Agda] generative thunk?   Conor McBride
• [Agda] generative thunk?   Nils Anders Danielsson
• [Agda] generative thunk?   Conor McBride

Last message date: Fri Dec 31 17:04:08 CEST 2010
Archived on: Fri Dec 31 17:04:13 CEST 2010

• Messages sorted by: [ thread ] [ subject ] [ author ]
• More info on this list...