2013 Archives by date

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

Starting: Tue Jan 1 13:38:29 CEST 2013
Ending: Tue Dec 31 15:48:55 CEST 2013
Messages: 1332

• [Agda] parsing reports   Serge D. Mechveliani
• Issue 777 [Re: [Agda] Semigroup.Carrier in 2.3.2]   Dominique Devriese
• [Agda] record syntax error   Serge D. Mechveliani
• [Agda] GandALF 2013 - Preliminary Call for Papers   Pietro Sala
• [Agda] 2nd CfP (deadline 14 Jan): Enabling Domain Experts to use Formalised Reasoning, Stage 2 (AISB 2013, Exeter, UK, 2-3 Apr 2013)   Christoph LANGE
• Bug 779 [Re: [Agda] record syntax error]   Andreas Abel
• Bug 779 [Re: [Agda] record syntax error]   Serge D. Mechveliani
• [Agda] issue 779   Serge D. Mechveliani
• [Agda] SLSP 2013: 2nd call for papers   GRLMC
• [Agda] ITP 2013: Last Call for Papers   David Pichardie
• [Agda] Ireland International Conference on Education (IICE-2013): Call for Papers!   L inda Woods
• [Agda] Setoid for List   Serge D. Mechveliani
• [Agda] LICS 2013 - Second Call for Workshop Proposals   Andrzej Murawski
• [Agda] type inference error?   Peter Divianszky
• [Agda] Setoid for List   Joachim Breitner
• [Agda] Setoid for List   Serge D. Mechveliani
• [Agda] Setoid for List   Dr. ERDI Gergo
• [Agda] Setoid for List   Joachim Breitner
• [Agda] type inference error?   Darryl
• [Agda] type inference error?   Andreas Abel
• [Agda] type inference error?   Jacques Carette
• [Agda] type inference error?   Andrés Sicard-Ramírez
• [Agda] type inference error?   Daniel Gustafsson
• [Agda] Agda on ghc-7.6.2-candidate   Serge D. Mechveliani
• [Agda] Agda on ghc-7.6.2-candidate   Andrés Sicard-Ramírez
• [Agda] Agda on ghc-7.6.2-candidate   Serge D. Mechveliani
• [Agda] standard instance proposal   Serge D. Mechveliani
• [Agda] Agda on ghc-7.6.2-candidate   Andrés Sicard-Ramírez
• [Agda] standard instance proposal   Dr. ÉRDI Gergő
• [Agda] standard instance proposal   Serge D. Mechveliani
• [Agda] TLCA 2013 Last Call for Papers   Luca Paolini
• [Agda] standard instance proposal   Serge D. Mechveliani
• [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
• [Agda] Deadline Extension (28 Jan): Enabling Domain Experts to use Formalised Reasoning, Stage 2 (AISB 2013, Exeter, UK, 2-5 Apr 2013)   Christoph LANGE
• [Agda] Classical Mathematics for a Constructive World   Andreas Abel
• [Agda] Classical Mathematics for a Constructive World   Peter Divianszky
• [Agda] missing record field   Serge D. Mechveliani
• [Agda] missing record field   James Chapman
• [Agda] missing record field   Dan Licata
• [Agda] Aquamacs pain   Liam O'Connor
• [Agda] WORLDCOMP: World’s Biggest Bogus Conference is Back Again   kelvinwilliams at hushmail.com
• [Agda] Aquamacs pain   Andreas Abel
• [Agda] Agda beginner   mukesh tiwari
• [Agda] Agda beginner   Guillaume Brunerie
• [Agda] Agda beginner   mukesh tiwari
• [Agda] Re: Agda beginner   mukesh tiwari
• [Agda] ARiSVe 2013 call for papers   Andrei Paskevich
• [Agda] Issue 508: Support Bird-style literate Agda   Peter Divianszky
• [Agda] Call for Registration: MGS Spring School   Alexander Kurz
• [Agda] Issue 508: Support Bird-style literate Agda   Andreas Abel
• [Agda] RTA 2013: LAST CALL FOR PAPERS   Sophie Tison
• [Agda] Type decidability   Dmytro Starosud
• [Agda] Type decidability   Daniel Peebles
• [Agda] new style mutual data broken?   Peter Divianszky
• [Agda] Type decidability   Dan Rosén
• [Agda] new style mutual data broken?   Adam Gundry
• [Agda] Type decidability   Dmytro Starosud
• [Agda] Type decidability   Dmytro Starosud
• [Agda] new style mutual data broken?   Peter Divianszky
• [Agda] Agda Tutorial darcs repo & pandoc backend   Peter Divianszky
• [Agda] lib solve f(x) = a   Serge D. Mechveliani
• [Agda] lib solve f(x) = a   Twan van Laarhoven
• [Agda] lib solve f(x) = a   Serge D. Mechveliani
• [Agda] lib solve f(x) = a   Twan van Laarhoven
• [Agda] tuple pattern sugar   Serge D. Mechveliani
• [Agda] tuple pattern sugar   Dmytro Starosud
• [Agda] tuple pattern sugar   Dmytro Starosud
• [Agda] tuple pattern sugar   Serge D. Mechveliani
• [Agda] tuple pattern sugar   Dmytro Starosud
• [Agda] PxTP 2013 - Call for Papers   Josef Urban
• [Agda] Datatype parameters and indices   Jan Malakhovski
• [Agda] tuple pattern sugar   Darryl
• [Agda] tuple pattern sugar   Serge D. Mechveliani
• [Agda] tuple pattern sugar   Andreas Abel
• [Agda] Datatype parameters and indices   Andreas Abel
• [Agda] Agda-mode problems in 2.3.2   Dominic Mulligan
• [Agda] Datatype parameters and indices   Jan Malakhovski
• [Agda] Agda-mode problems in 2.3.2   Peter Divianszky
• [Agda] SSTiC 2013: 1st announcement   GRLMC
• [Agda] Datatype parameters and indices   Andreas Abel
• [Agda] Datatype parameters and indices   Darryl
• [Agda] -> and let in syntax definitions   Darryl
• [Agda] -> and let in syntax definitions   Andreas Abel
• [Agda] Status of copatterns   Francesco Mazzoli
• [Agda] Datatype parameters and indices   Jan Malakhovski
• [Agda] Re: Status of copatterns   Andreas Abel
• [Agda] VSC call for paper: DEADLINE EXTENDED   Andrea Calvagna
• [Agda] Agda-mode problems in 2.3.2   Dominic Mulligan
• [Agda] implicit level arguments   Serge D. Mechveliani
• [Agda] Computation and patterns in called functions   Francesco Mazzoli
• [Agda] Re: Computation and patterns in called functions   Francesco Mazzoli
• [Agda] tuple pattern sugar   Nils Anders Danielsson
• [Agda] ITP 2013 - Deadline Extension   David Pichardie
• [Agda] proof overhead   Nils Anders Danielsson
• [Agda] parsing reports   Nils Anders Danielsson
• [Agda] Setoid for List   Nils Anders Danielsson
• [Agda] standard instance proposal   Nils Anders Danielsson
• [Agda] Agda Tutorial darcs repo & pandoc backend   Nils Anders Danielsson
• [Agda] implicit level arguments   Nils Anders Danielsson
• [Agda] parsing reports   Serge D. Mechveliani
• [Agda] Computation and patterns in called functions   Nils Anders Danielsson
• [Agda] Agda-mode problems in 2.3.2   Nils Anders Danielsson
• [Agda] Computation and patterns in called functions   Francesco Mazzoli
• [Agda] Re: Computation and patterns in called functions   Francesco Mazzoli
• [Agda] Computation and patterns in called functions   Nils Anders Danielsson
• [Agda] Computation and patterns in called functions   Francesco Mazzoli
• [Agda] tuple pattern sugar   Wolfram Kahl
• [Agda] Re: Computation and patterns in called functions   Francesco Mazzoli
• [Agda] Cost of ``open ... public using (...)''?   Wolfram Kahl
• [Agda] Cost of ``open ... public using (...)''?   Nils Anders Danielsson
• [Agda] tuple pattern sugar   Nils Anders Danielsson
• [Agda] World’s Biggest Computer Conference WORLDCOMP is Cancelled   amgsolo at hushmail.com
• [Agda] ANNOUNCE: Standard library version 0.7   Nils Anders Danielsson
• [Agda] lib-0.7 vs lib-0.6   Serge D. Mechveliani
• [Agda] Another Data.List.Any - Is it possible?   Dmytro Starosud
• [Agda] Computation and patterns in called functions   James Deikun
• [Agda] Another Data.List.Any - Is it possible?   Arseniy Alekseyev
• [Agda] Another Data.List.Any - Is it possible?   Dmytro Starosud
• [Agda] lib-0.7 vs lib-0.6   Nils Anders Danielsson
• [Agda] Subsetoid, Subgroup ...   Serge D. Mechveliani
• [Agda] Subsetoid, Subgroup ...   Nils Anders Danielsson
• [Agda] function application in index positions   Peter Divianszky
• [Agda] function application in index positions   Alan Jeffrey
• [Agda] C-style macros in Agda :)   Dmytro Starosud
• [Agda] Re: C-style macros in Agda :)   Dmytro Starosud
• [Agda] Re: C-style macros in Agda :)   Dmytro Starosud
• [Agda] predicate for sub-type   Serge D. Mechveliani
• [Agda] predicate for sub-type   Andreas Abel
• [Agda] Re: C-style macros in Agda :)   Andreas Abel
• [Agda] Re: C-style macros in Agda :)   Dmytro Starosud
• [Agda] \member vs \notin   Serge D. Mechveliani
• [Agda] \member vs \notin   Andrés Sicard-Ramírez
• [Agda] function application in index positions   Andreas Abel
• [Agda] C-style macros in Agda :)   Nils Anders Danielsson
• [Agda] sentences in a line   Serge D. Mechveliani
• [Agda] sentences in a line   Nils Anders Danielsson
• [Agda] C-style macros in Agda :)   Dmytro Starosud
• [Agda] C-style macros in Agda :)   Nils Anders Danielsson
• [Agda] Joint Call For Papers - Conferences / Journal Special Issues, February 2013)   cfp at grid.chu.edu.tw
• [Agda] xs\_A   Serge D. Mechveliani
• [Agda] xs\_A   Liam O'Connor
• [Agda] xs\_A   Jean-Philippe Bernardy
• [Agda] function application in index positions   Peter Divianszky
• [Agda] Re: xs\_A   Stefan Monnier
• [Agda] function application in index positions   Andreas Abel
• [Agda] dangerous _$_   Serge D. Mechveliani
• [Agda] dangerous _$_   Andreas Abel
• [Agda] agda-executable depricated   Peter Divianszky
• [Agda] newest agda dependencies   Peter Divianszky
• [Agda] newest agda dependencies   Andreas Abel
• [Agda] newest agda dependencies   PÁLI Gábor János
• [Agda] newest agda dependencies   Andreas Abel
• [Agda] newest agda dependencies   Nils Anders Danielsson
• [Agda] difficult "unsolved metas"   Serge D. Mechveliani
• [Agda] newest agda dependencies   Peter Divianszky
• [Agda] difficult "unsolved metas"   Serge D. Mechveliani
• [Agda] SLSP 2013: 3rd call for papers   GRLMC
• [Agda] difficult "unsolved metas"   Nils Anders Danielsson
• [Agda] ICFP 2013: Call for papers   David Van Horn
• [Agda] difficult "unsolved metas"   Serge D. Mechveliani
• [Agda] newest agda dependencies   Wolfram Kahl
• [Agda] 1st CFP SBLP 2013 (17th Brazilian Symposium on Programming Languages)   Andre Du Bois
• [Agda] preserving predicate   Serge D. Mechveliani
• [Agda] preserving predicate   Serge D. Mechveliani
• [Agda] preserving predicate   Nils Anders Danielsson
• [Agda] preserving predicate   Darryl McAdams
• [Agda] no-field record   Serge D. Mechveliani
• [Agda] no-field record   Andreas Abel
• [Agda] CSL 2013 first call-for-papers   Ronchi Della Rocca Simona
• [Agda] A Ph.D. Student’s CRY for Help   saidi34 at hushmail.com
• [Agda] DICE 2013 - call-for partcipation   Simona Ronchi della Rocca
• [Agda] First steps in agda   Mathijs Kwik
• [Agda] Second Call For Papers: Conf. Intelligent Computer Mathematics (CICM 2013), July 8-12, 2013, Bath, UK   Serge Autexier
• [Agda] First steps in agda   Andreas Abel
• [Agda] Workshop Haskell and Rewriting Techniques HART 2013   Janis Voigtländer
• [Agda] Can rigid variables be treated as constructors/postulates?   Arseniy Alekseyev
• [Agda] exhaustive patterns   Serge D. Mechveliani
• [Agda] Can rigid variables be treated as constructors/postulates?   Andreas Abel
• [Agda] exhaustive patterns   Andreas Abel
• [Agda] Can rigid variables be treated as constructors/postulates?   Darryl McAdams
• [Agda] exhaustive patterns   Serge D. Mechveliani
• [Agda] PhD Positions in Formal Methods and Language-based Security at Chalmers   Ana Bove
• [Agda] proof by AC-reduction   Serge D. Mechveliani
• [Agda] reexport from record   Serge D. Mechveliani
• [Agda] Participate: Enabling Domain Experts to use Formalised Reasoning (AISB 2013, Exeter, UK, 3-5 Apr 2013). Tutorials on Matching, Auctions, Finance.   Christoph LANGE
• open public in record [Re: [Agda] reexport from record]   Andreas Abel
• [Agda] proof by AC-reduction   Nils Anders Danielsson
• [Agda] proof by AC-reduction   Dan Rosén
• [Agda] IICAI-13 Call for papers   Venkateswara Rao
• [Agda] proof by AC-reduction   Serge D. Mechveliani
• [Agda] proof by AC-reduction   Serge D. Mechveliani
• [Agda] Joint Call For Papers - Conferences / Journal Special Issues, February 2013, 2nd update)   cfp at grid.chu.edu.tw
• [Agda] LATA 2013: call for participation   GRLMC
• [Agda] `reasoninig' example   Serge D. Mechveliani
• [Agda] Agda Tutorial darcs repo & pandoc backend   Peter Divianszky
• [Agda] duplicate builtin natural, succ, zero   Peter Divianszky
• [Agda] AIM XVII in Shonan, Wed, 8 May - 13 May 2013   KINOSHITA Yoshiki
• [Agda] duplicate builtin natural, succ, zero   Andreas Abel
• [Agda] duplicate builtin natural, succ, zero   Peter Divianszky
• [Agda] duplicate builtin natural, succ, zero   Peter Divianszky
• [Agda] duplicate builtin natural, succ, zero   Nils Anders Danielsson
• [Agda] `reasoninig' example   Nils Anders Danielsson
• [Agda] Agda Tutorial darcs repo & pandoc backend   Nils Anders Danielsson
• [Agda] failure of reduction inside an abstract block   Paolo Capriotti
• [Agda] failure of reduction inside an abstract block   Andreas Abel
• [Agda] Call for Papers: Canada International Conference on Education (CICE-2013)!   Margaret Smith
• [Agda] failure of reduction inside an abstract block   Paolo Capriotti
• [Agda] Final Call for Papers: Ireland International Conference on Education (IICE-2013)!   L inda Woods
• [Agda] Agda Tutorial darcs repo & pandoc backend   Peter Divianszky
• [Agda] IT Workshop Submission Deadline 10 March: IEEE Xplore/EI Compendex/ISI   X.F. Meng
• [Agda] "with .. postulate"   Serge D. Mechveliani
• [Agda] SLSP 2013: submission deadline extended   GRLMC
• [Agda] "with .. postulate"   Andreas Abel
• [Agda] Avoiding η-contraction   Andrés Sicard-Ramírez
• [Agda] Avoiding η-contraction   Andreas Abel
• [Agda] IT Workshop Submission Deadline 10 March: IEEE Xplore/EI Compendex/ISI   X.F. Meng
• [Agda] EqReasoning example   Serge D. Mechveliani
• Re: [Agda] Avoiding η-contraction   Andrés Sicard-Ramírez
• [Agda] EqReasoning example   Andreas Abel
• [Agda] instance arguments proposal and crash   Paolo Capriotti
• [Agda] EqReasoning example   Serge D. Mechveliani
• [Agda] EqReasoning example   Serge D. Mechveliani
• [Agda] ARiSVe 2013 final call for papers   Andrei Paskevich
• [Agda] Research Assistantship at Oxford on Bidirectional Transformations   Jeremy.Gibbons at cs.ox.ac.uk
• [Agda] instance arguments proposal and crash   Dominique Devriese
• [Agda] instance arguments proposal and crash   Paolo Capriotti
• [Agda] "with .. postulate"   Serge D. Mechveliani
• [Agda] with match changes the result type of a function   Dominique Devriese
• [Agda] instance arguments proposal and crash   Andreas Abel
• [Agda] instance arguments proposal and crash   Paolo Capriotti
• [Agda] "with .. postulate"   Andreas Abel
• [Agda] "with .. postulate"   Andreas Abel
• [Agda] with match changes the result type of a function   Serge D. Mechveliani
• [Agda] with match changes the result type of a function   Andreas Abel
• [Agda] with match changes the result type of a function   Darryl McAdams
• [Agda] "with .. postulate"   Serge D. Mechveliani
• [Agda] Deadline Extension March 12th, 2013: Conf. Intelligent Computer Mathematics (CICM 2013), July 8-12, 2013, Bath, UK   Serge Autexier
• [Agda] with match changes the result type of a function   Andreas Abel
• [Agda] "with .. postulate"   Andreas Abel
• [Agda] with match changes the result type of a function   Darryl McAdams
• [Agda] with match changes the result type of a function   Dominique Devriese
• [Agda] Termination checking regression (Matrix-shaped orders?)   Dominique Devriese
• [Agda] Termination checking regression (Matrix-shaped orders?)   Andrés Sicard-Ramírez
• [Agda] Termination checking regression (Matrix-shaped orders?)   Nils Anders Danielsson
• [Agda] "with .. postulate"   Serge D. Mechveliani
• [Agda] Termination checking regression (Matrix-shaped orders?)   Dominique Devriese
• [Agda] eta expansion   Martin Escardo
• [Agda] eta expansion   Andreas Abel
• [Agda] eta expansion   Andrés Sicard-Ramírez
• [Agda] eta expansion   Peter Hancock
• [Agda] eta expansion   Martin Escardo
• [Agda] eta expansion   Nils Anders Danielsson
• [Agda] eta expansion   Martin Escardo
• [Agda] eta expansion   Martin Escardo
• [Agda] eta expansion   Andrés Sicard-Ramírez
• [Agda] eta expansion   Martin Escardo
• [Agda] eta expansion   Peter Hancock
• [Agda] eta expansion   Andreas Abel
• [Agda] eta expansion   Vladimir Voevodsky
• [Agda] Joint Call For Papers - Conferences / Journal Special Issues, March 2013)   cfp at grid.chu.edu.tw
• [Agda] eta expansion   Dan Licata
• [Agda] SSTiC 2013: 2nd announcement   GRLMC
• [Agda] eta expansion   Peter Hancock
• [Agda] eta expansion   Andreas Abel
• [Agda] false \equiv true   Serge D. Mechveliani
• [Agda] false \equiv true   Adam Gundry
• [Agda] eta expansion   Nils Anders Danielsson
• [Agda] eta expansion   Martin Escardo
• [Agda] eta expansion   Martin Escardo
• [Agda] ARiSVe 2013: submission deadline extension to April 8, 2013   Andrei Paskevich
• [Agda] CfP PLMMS at CICM, July 2013, Bath, UK   Iain Whiteside
• [Agda] unclear import report   Serge D. Mechveliani
• [Agda] Simple contradiction from type-in-type   Samuel Gélineau
• [Agda] CSL'13, last cfp, DATES POSTPONED!!   Simona Ronchi della Rocca
• [Agda] Simple contradiction from type-in-type   Dominique Devriese
• [Agda] Simple contradiction from type-in-type   Andreas Abel
• [Agda] Simple contradiction from type-in-type   Dominique Devriese
• [Agda] Simple contradiction from type-in-type   Andreas Abel
• [Agda] unclear import report   Nils Anders Danielsson
• [Agda] Workshop on Generic Programming (WGP 2013) -- call for papers   Jeremiah Willcock
• [Agda] CFP: AIM XVII in Shonan, Japan   木下 佳樹
• [Agda] ICFP 2013: Second Call for Papers   David Van Horn
• [Agda] Joint Call For Papers - Conferences / Journal Special Issues (March 2013, 2nd update)   cfp at grid.chu.edu.tw
• [Agda] Joint Call For Papers - Conferences / Journal Special Issues (March 2013, 2nd update)   Gabriel Scherer
• [Agda] Joint Call For Papers - Conferences / Journal Special Issues (March 2013, 2nd update)   Ulf Norell
• [Agda] blowUpSparseVec error   Darryl McAdams
• [Agda] PPDP 2013: Call for Papers   Steven Keuchel
• [Agda] Postdoctoral Research Positions   Dan Ghica
• [Agda] blowUpSparseVec error   Nils Anders Danielsson
• [Agda] blowUpSparseVec error   Darryl McAdams
• [Agda] blowUpSparseVec error   Andreas Abel
• [Agda] eta expansion   Peter Hancock
• [Agda] Re: eta expansion   Francesco Mazzoli
• [Agda] eta expansion   Peter LeFanu Lumsdaine
• [Agda] Re: eta expansion   Francesco Mazzoli
• [Agda] Re: eta expansion   Peter Hancock
• [Agda] Re: eta expansion   Altenkirch Thorsten
• [Agda] Re: eta expansion   Martin Escardo
• [Agda] Re: eta expansion   Altenkirch Thorsten
• [Agda] Re: eta expansion   Peter Hancock
• [Agda] 2nd CFP: SBLP 2013 (17th Brazilian Symposium on Programming Languages)   Andre Du Bois
• [Agda] LOLA 2013: Call for Talk Proposals   Andrew Kennedy
• [Agda] Friday afternoon magic   Nils Anders Danielsson
• [Agda] Ackermann Award 2013 - Call for Nominations   Anuj Dawar
• [Agda] Oregon Programming Languages Summer School - call for participation   Amal Ahmed
• [Agda] introductory book   washington3 at countermail.com
• [Agda] Friday afternoon magic   Andreas Abel
• [Agda] introductory book   Darryl McAdams
• [Agda] Oregon Programming Languages Summer School - call for participation   Darryl McAdams
• [Agda] introductory book   Nils Anders Danielsson
• [Agda] SSTiC 2013: 2nd registration deadline 26 March   GRLMC
• [Agda] introductory book   Peter Divianszky
• [Agda] WORLDCOMP fake conference   washington3 at countermail.com
• [Agda] Run Agda program   Mikuláš Knut
• [Agda] A Demonstration of Agda by Alan Jeffrey   mukesh tiwari
• [Agda] A Demonstration of Agda by Alan Jeffrey   Guillaume Brunerie
• [Agda] A Demonstration of Agda by Alan Jeffrey   Nils Anders Danielsson
• [Agda] Re: A Demonstration of Agda by Alan Jeffrey   mukesh tiwari
• [Agda] A Demonstration of Agda by Alan Jeffrey   Peter Hancock
• [Agda] Run Agda program   Dmytro Starosud
• [Agda] A Demonstration of Agda by Alan Jeffrey   mukesh tiwari
• [Agda] (CFP) Certified Programs and Proofs 2013 - First Call for Papers   Bas Spitters
• [Agda] INTECH 2013   edprocess
• [Agda] Types Meeting 2013 in Toulouse, 22 - 26 April: 2nd call for participation   Ralph Matthes
• [Agda] multiple compilation   Serge D. Mechveliani
• [Agda] multiple compilation   Andrés Sicard-Ramírez
• [Agda] multiple compilation   Serge D. Mechveliani
• [Agda] multiple compilation   Andrés Sicard-Ramírez
• [Agda] multiple compilation   Serge D. Mechveliani
• [Agda] expressing iff   Serge D. Mechveliani
• [Agda] Stymied by a proof irrelevance requirement   Jacques Carette
• [Agda] LICS 2013 - Call for Short Presentations   Andrzej Murawski
• [Agda] Stymied by a proof irrelevance requirement   Wolfram Kahl
• [Agda] Stymied by a proof irrelevance requirement   Jacques Carette
• [Agda] expressing iff   Andreas Abel
• [Agda] expressing iff   Serge D. Mechveliani
• [Agda] Stymied by a proof irrelevance requirement   Nils Anders Danielsson
• [Agda] expressing iff   Nils Anders Danielsson
• [Agda] Markdown and Agda   Francesco Mazzoli
• [Agda] Re: Markdown and Agda   Francesco Mazzoli
• [Agda] result code explosion   Serge D. Mechveliani
• [Agda] Markdown and Agda   Francesco Mazzoli
• [Agda] Re: _iff_   Serge D. Mechveliani
• [Agda] APLAS 2013 call for papers   Chung-chieh Shan
• [Agda] ICDIM 2013   edprocess
• [Agda] Stymied by a proof irrelevance requirement   Dan Licata
• [Agda] result code explosion   Nils Anders Danielsson
• [Agda] multiple compilation   Nils Anders Danielsson
• [Agda] result code explosion   Serge D. Mechveliani
• [Agda] Call for talk proposals: HOPE'13 (Workshop on Higher-Order Programming with Effects, affiliated with ICFP'13)   Hongseok Yang
• [Agda] multiple compilation   Serge D. Mechveliani
• [Agda] Stymied by a proof irrelevance requirement   Andreas Abel
• [Agda] Stymied by a proof irrelevance requirement   Guillaume Brunerie
• [Agda] Stymied by a proof irrelevance requirement   Conor McBride
• [Agda] multiple compilation   Nils Anders Danielsson
• [Agda] multiple compilation   Serge D. Mechveliani
• [Agda] DTP 2013 Call for Papers   Stephanie Weirich
• [Agda] multiple compilation   Nils Anders Danielsson
• [Agda] neg ~~   Serge D. Mechveliani
• [Agda] refl and pattern matching   Andrés Sicard-Ramírez
• [Agda] refl and pattern matching   Martin Escardo
• [Agda] neg ~~   Nils Anders Danielsson
• [Agda] neg ~~   Nils Anders Danielsson
• [Agda] Enumeration of Binary Trees   Dima Zhyltsov
• [Agda] Preserves-by-2-of-3   Serge D. Mechveliani
• [Agda] Preserves-by-2-of-3   Arseniy Alekseyev
• [Agda] Preserves-by-2-of-3   Serge D. Mechveliani
• [Agda] SBLP 2013: Final CFP, deadline for Abstracts 19/4   Andre Du Bois
• [Agda] Microsoft-funded PhD opportunity (software/ system verification)   Tom Ridge
• [Agda] recursive \times   Serge D. Mechveliani
• [Agda] recursive \times   Dr. ÉRDI Gergő
• [Agda] ITP 2013: Call for Participation   David Pichardie
• [Agda] CfP PLMMS at CICM, July 2013, Bath, UK   Iain Whiteside
• [Agda] CfP PLMMS at CICM, July 2013, Bath, UK   Iain Whiteside
• [Agda] LFMTP'13: Call for papers   Brigitte Pientka
• [Agda] recursive \times   Andreas Abel
• [Agda] String -> Nat   Serge D. Mechveliani
• [Agda] list of types   Serge D. Mechveliani
• [Agda] list of types   Andreas Abel
• [Agda] String -> Nat   Andreas Abel
• [Agda] String -> Nat   Serge D. Mechveliani
• [Agda] list of types   Altenkirch Thorsten
• [Agda] list of types   Altenkirch Thorsten
• [Agda] list of types   Altenkirch Thorsten
• [Agda] list of types   Twan van Laarhoven
• [Agda] list of types   Altenkirch Thorsten
• [Agda] list of types   Bas Spitters
• [Agda] list of types   Altenkirch Thorsten
• [Agda] Re: String -> Nat   Benjamin Barenblat
• [Agda] failed constraint   Serge D. Mechveliani
• [Agda] failed constraint   Andrés Sicard-Ramírez
• [Agda] Re: String -> Nat   Nils Anders Danielsson
• [Agda] Does Agda compiler read haskell's type information?   Станислав Черничкин
• [Agda] Does Agda compiler read haskell's type information?   Nils Anders Danielsson
• [Agda] Re: CFP: AIM XVII in Shonan, Japan   木下 佳樹
• [Agda] Oregon PL Summer School: register by April 30th   Amal Ahmed
• [Agda] RA positions at Imperial   Gardner, Philippa A
• [Agda] Re: Markdown and Agda   Francesco Mazzoli
• [Agda] Using functions before its declaration   Amila Jayasekara
• [Agda] Using functions before its declaration   Dmytro Starosud
• [Agda] Using functions before its declaration   Guillaume Brunerie
• [Agda] failed constraint   Serge D. Mechveliani
• [Agda] failed constraint   Nils Anders Danielsson
• [Agda] tenure-track position in Theoretical Computer Science   Femke van Raamsdonk
• [Agda] 4 Assistant / Associate Professors in Computer Science (Tenure track)   Ana Bove
• [Agda] Using functions before its declaration   Amila Jayasekara
• [Agda] Where clauses   Andrés Sicard-Ramírez
• [Agda] Where clauses   Andreas Abel
• [Agda] Where clauses   Andrés Sicard-Ramírez
• [Agda] CfP: OpenMath workshop at CICM (10 July, Bath, UK), submission deadline 7 June   Christoph LANGE
• [Agda] Where clauses   Daniel Peebles
• [Agda] Agda Intensive Meeting (AIM XVII) registration closing soon   木下 佳樹
• [Agda] Infinite proofs   Yasuyuki Ogawa
• [Agda] Infinite proofs   Daniel Peebles
• [Agda] failed constraint   Serge D. Mechveliani
• [Agda] Infinite proofs   Paolo Capriotti
• [Agda] Infinite proofs   Yasuyuki Ogawa
• [Agda] Infinite proofs   Yasuyuki Ogawa
• [Agda] TPNC 2013: 1st call for papers   GRLMC
• [Agda] failed constraint   Nils Anders Danielsson
• [Agda] CFP SBLP 2013: Deadline extension   Andre Du Bois
• [Agda] AIM XVII registration being closed   木下 佳樹
• [Agda] Where clauses   Owen
• [Agda] Where clauses   Guillaume Brunerie
• [Agda] c-c c-l + import   Serge D. Mechveliani
• [Agda] c-c c-l + import   gallais
• [Agda] Where clauses   Daniel Peebles
• [Agda] ------ GandALF 2013 ----- FINAL CALL FOR PAPERS -----   Pietro Sala
• [Agda] c-c c-l + import   Serge D. Mechveliani
• [Agda] What is the type of the diagonal function?   Jacques Carette
• [Agda] What is the type of the diagonal function?   Andreas Abel
• [Agda] What is the type of the diagonal function?   Jacques Carette
• [Agda] Agda 2.3.2 installation in ubuntu 12.04   Martin Escardo
• [Agda] Agda 2.3.2 installation in ubuntu 12.04   Nils Anders Danielsson
• [Agda] Agda 2.3.2 installation in ubuntu 12.04   gallais
• [Agda] Agda 2.3.2 installation in ubuntu 12.04   Nils Anders Danielsson
• [Agda] CiE 2013 - 2nd Call for Informal Presentations   S B Cooper
• [Agda] Understanding the pattern matching in proofs   Amila Jayasekara
• [Agda] Maybe-like combinator for propositions   Dr. ERDI Gergo
• [Agda] Maybe-like combinator for propositions   Daniel Peebles
• [Agda] Does Agda compiler read haskell's type information?   Wolfgang Jeltsch
• [Agda] Does Agda compiler read haskell's type information?   Wolfgang Jeltsch
• [Agda] stack overflow when type check   Sergei Meshveliani
• [Agda] stack overflow when type check   Andrés Sicard-Ramírez
• [Agda] Understanding the pattern matching in proofs   Nils Anders Danielsson
• [Agda] Understanding the pattern matching in proofs   Amila Jayasekara
• [Agda] stack overflow when type check   Sergei Meshveliani
• [Agda] Thematic trimester "Semantics of proofs and certified mathematics", spring 2014, Paris   Pierre-Louis Curien
• [Agda] LICS 2013 - Call for Participation   Andrzej Murawski
• [Agda] type of identifier   Sergei Meshveliani
• [Agda] Fwd: Two PhD student positions in Gothenburg   Aarne Ranta
• [Agda] Fwd: Two post doctor positions in Gothenburg in Computer science: Language Technology and Formal Methods   Aarne Ranta
• [Agda] Re: type of identifier   Francesco Mazzoli
• [Agda] SSTiC 2013: next registration deadline 26 May   GRLMC
• [Agda] MCS: Formal Proofs for Mathematics and Computer Science [Call for Papers]   Laurent Théry
• [Agda] memory eagerness   Sergei Meshveliani
• [Agda] memory eagerness   Wolfram Kahl
• [Agda] ------ GandALF 2013 ----- FINAL CALL FOR PAPERS (EXTENDED DEADLINE)-----   Pietro Sala
• [Agda] memory eagerness   Sergei Meshveliani
• [Agda] Termination checker correctness proof   Jesper Cockx
• [Agda] Termination checker correctness proof   Altenkirch Thorsten
• [Agda] Termination checker correctness proof   Nils Anders Danielsson
• [Agda] Termination checker correctness proof   Jesper Cockx
• [Agda] *Deadline Extension* PLMMS, 9th July 2013, Bath, UK   Iain Whiteside
• [Agda] record field ambiguity   Sergei Meshveliani
• [Agda] Agda IO program: how to turn off buffering?   stvienna wiener
• [Agda] Agda IO program: how to turn off buffering?   Andrés Sicard-Ramírez
• [Agda] Call for talk proposals: HOPE'13 (Workshop on Higher-Order Programming with Effects, affiliated with ICFP'13)   Hongseok Yang
• [Agda] Implementation of abstract vs. irrelevance   Andrea Vezzosi
• [Agda] Implementation of abstract vs. irrelevance   Andreas Abel
• [Agda] Instance arguments and hole types   Tillmann Rendel
• [Agda] Instance arguments and hole types   Nils Anders Danielsson
• [Agda] record field ambiguity   Nils Anders Danielsson
• [Agda] memory eagerness   Nils Anders Danielsson
• [Agda] Implementation of abstract vs. irrelevance   Andrea Vezzosi
• [Agda] Instance arguments and hole types   Tillmann Rendel
• [Agda] RDP 2013 Call for Participation   Luca Paolini
• [Agda] `abstract' on Web keywords   Sergei Meshveliani
• [Agda] Instance arguments and hole types   Nils Anders Danielsson
• [Agda] `abstract' on Web keywords   Nils Anders Danielsson
• [Agda] `abstract' on Web keywords   Sergei Meshveliani
• [Agda] `abstract' on Web keywords   Sergei Meshveliani
• [Agda] `abstract' on Web keywords   Nils Anders Danielsson
• [Agda] `abstract' on Web keywords   Serge D. Mechveliani
• [Agda] Defining a module by pattern matching   Guillaume Brunerie
• [Agda] Defining a module by pattern matching   Dr. ERDI Gergo
• [Agda] Defining a module by pattern matching   Guillaume Brunerie
• [Agda] Defining a module by pattern matching   Dr. ERDI Gergo
• [Agda] Defining a module by pattern matching   Nils Anders Danielsson
• [Agda] Defining a module by pattern matching   Guillaume Brunerie
• [Agda] Defining a module by pattern matching   Andreas Abel
• [Agda] CiE 2013 in Milan, July 1 - 5: First Call for Participation   S B Cooper
• [Agda] DTP 2013 2nd Call For Papers   Stephanie Weirich
• [Agda] Implementation of abstract vs. irrelevance   Andrea Vezzosi
• [Agda] Final CFP: INTECH 2013 at BCS   edprocess
• [Agda] isHead x (x :: xs)   Sergei Meshveliani
• [Agda] isHead x (x :: xs)   Paolo Capriotti
• [Agda] MFPS/LICS/CSF Joint Call for Participation   Andrzej Murawski
• [Agda] LCC'13 : Workshop on Logic and Computational Complexity   Arnaud Durand
• [Agda] SSTiC 2013: next registration deadline 26 May   GRLMC
• [Agda] 2nd CfP: OpenMath workshop at CICM (10 July, Bath, UK), submission deadline 7 June   Christoph LANGE
• [Agda] LFMTP'13: Logical Frameworks and Meta-Languages (CFP)   Brigitte Pientka
• [Agda] Absurd question   Martin Escardo
• [Agda] Absurd question   Guillaume Brunerie
• [Agda] Absurd question   Martin Escardo
• [Agda] Absurd question   Martin Escardo
• [Agda] Absurd question   Martin Escardo
• [Agda] Absurd question   Andrea Vezzosi
• [Agda] Absurd question   Martin Escardo
• [Agda] Absurd question   Wolfram Kahl
• [Agda] Absurd question   Andrea Vezzosi
• [Agda] Absurd question   Martin Escardo
• [Agda] Absurd question   Andreas Abel
• [Agda] Absurd question   Martin Escardo
• [Agda] Conference "Type Theory, Homotopy Theory and Univalent Foundations"   Nicola Gambino
• [Agda] Call for Papers IFL 2013   publicityifl at gmail.com
• [Agda] `abstract' on Web keywords   Nils Anders Danielsson
• [Agda] CFP: Relational and Algebraic Methods in Computer Science (RAMiCS 2014)   Peter Höfner
• [Agda] --without-K option too restrictive?   Andrés Sicard-Ramírez
• [Agda] Workshop on Generic Programming (WGP 2013) -- second call for papers (due June 14)   Jeremiah Willcock
• [Agda] --without-K option too restrictive?   Dmytro Starosud
• [Agda] --without-K option too restrictive?   Nils Anders Danielsson
• [Agda] --without-K option too restrictive?   Jason Gross
• [Agda] --without-K option too restrictive?   Andrés Sicard-Ramírez
• [Agda] --without-K option too restrictive?   Dan Licata
• [Agda] --without-K option too restrictive?   Andrés Sicard-Ramírez
• [Agda] --without-K option too restrictive?   Andreas Abel
• [Agda] --without-K option too restrictive?   Andreas Abel
• [Agda] --without-K option too restrictive?   Andrés Sicard-Ramírez
• [Agda] --without-K option too restrictive?   Martin Escardo
• [Agda] Fwd: [Haskell-cafe] Problem with compilation on MAC OS X   Simon Thompson
• [Agda] Fwd: [Haskell-cafe] Problem with compilation on MAC OS X   Simon Thompson
• Less restrictive --without-K [Re: [Agda] no longer type checks]   Andreas Abel
• [Agda] --without-K option too restrictive?   Andreas Abel
• [Agda] Fwd: [Haskell-cafe] Problem with compilation on MAC OS X   Nils Anders Danielsson
• [Agda] [Haskell-cafe] Problem with compilation on MAC OS X   Simon Thompson
• [Agda] --without-K option too restrictive?   Nils Anders Danielsson
• [Agda] [Haskell-cafe] Problem with compilation on MAC OS X   Simon Thompson
• Less restrictive --without-K [Re: [Agda] no longer type checks]   Nils Anders Danielsson
• Less restrictive --without-K [Re: [Agda] no longer type checks]   Andrés Sicard-Ramírez
• Less restrictive --without-K [Re: [Agda] no longer type checks]   Nils Anders Danielsson
• Less restrictive --without-K [Re: [Agda] no longer type checks]   Andreas Abel
• Less restrictive --without-K [Re: [Agda] no longer type checks]   Andreas Abel
• Less restrictive --without-K [Re: [Agda] no longer type checks]   Andrés Sicard-Ramírez
• Less restrictive --without-K [Re: [Agda] no longer type checks]   Andreas Abel
• [Agda] refusal to construct infinite term   Martin Escardo
• [Agda] Call for Papers IFL 2013   publicityifl at gmail.com
• [Agda] refusal to construct infinite term   Andrés Sicard-Ramírez
• Less restrictive --without-K [Re: [Agda] no longer type checks]   Andrés Sicard-Ramírez
• [Agda] with - refl strangeness   Sergei Meshveliani
• [Agda] Haskell 2013 second call for submissions   Chung-chieh Shan
• [Agda] APLAS 2013 second call for papers   Chung-chieh Shan
• [Agda] with - refl strangeness   Dominique Devriese
• [Agda] with - refl strangeness   Andreas Abel
• Less restrictive --without-K [Re: [Agda] no longer type checks]   Nils Anders Danielsson
• Less restrictive --without-K [Re: [Agda] no longer type checks]   Andreas Abel
• [Agda] `divides' definition   Sergei Meshveliani
• [Agda] `divides' definition   Nils Anders Danielsson
• [Agda] Trust me regarding Dan Licata's trick   Martin Escardo
• [Agda] Trust me regarding Dan Licata's trick   Guillaume Brunerie
• [Agda] Trust me regarding Dan Licata's trick   Martin Escardo
• [Agda] Trust me regarding Dan Licata's trick   Dan Licata
• [Agda] Trust me regarding Dan Licata's trick   Martin Escardo
• [Agda] Trust me regarding Dan Licata's trick   Guillaume Brunerie
• [Agda] Trust me regarding Dan Licata's trick   Martin Escardo
• [Agda] Trust me regarding Dan Licata's trick   Guillaume Brunerie
• [Agda] Trust me regarding Dan Licata's trick   Nils Anders Danielsson
• [Agda] Trust me regarding Dan Licata's trick   Alan Jeffrey
• [Agda] Trust me regarding Dan Licata's trick   Nils Anders Danielsson
• [Agda] Trust me regarding Dan Licata's trick   Martin Escardo
• [Agda] Trust me regarding Dan Licata's trick   Guillaume Brunerie
• [Agda] FLoC 2014 Call for Workshops (The Sixth Federated Logic Conference, July 2014, Vienna, Austria)   David Pichardie
• [Agda] Trust me regarding Dan Licata's trick   Guillaume Brunerie
• [Agda] Trust me regarding Dan Licata's trick   Martin Escardo
• [Agda] Trust me regarding Dan Licata's trick   Guillaume Brunerie
• [Agda] Trust me regarding Dan Licata's trick   Martin Escardo
• [Agda] ITP 2013 Call for Participation (Early Registration Deadline June 17th)   David Pichardie
• [Agda] Trust me regarding Dan Licata's trick   Peter Hancock
• [Agda] Trust me regarding Dan Licata's trick   Martin Escardo
• [Agda] Trust me regarding Dan Licata's trick   Conor McBride
• [Agda] Trust me regarding Dan Licata's trick   Nils Anders Danielsson
• [Agda] Trust me regarding Dan Licata's trick   Martin Escardo
• [Agda] ANNOUNCE: Agda 2.3.2.1   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.3.2.1   Andreas Abel
• [Agda] ANNOUNCE: Agda 2.3.2.1   Andrés Sicard-Ramírez
• [Agda] Trust me regarding Dan Licata's trick   Martin Escardo
• [Agda] Re: ANNOUNCE: Agda 2.3.2.1   Andrés Sicard-Ramírez
• [Agda] Trust me regarding Dan Licata's trick   Dan Licata
• [Agda] Call for Papers IFL 2013   publicityifl at gmail.com
• [Agda] Trust me regarding Dan Licata's trick   Martin Escardo
• [Agda] Trust me regarding Dan Licata's trick   Bas Spitters
• [Agda] Vec _ n cong by n   Sergei Meshveliani
• [Agda] Re: Vec _ n cong by n   Francesco Mazzoli
• [Agda] Vec _ n cong by n   Jesper Cockx
• [Agda] Vec _ n cong by n   Sergei Meshveliani
• [Agda] Vec _ n cong by n   Jesper Cockx
• [Agda] Vec _ n cong by n   Sergei Meshveliani
• [Agda] Vec _ n cong by n   Paolo Capriotti
• [Agda] congruence on dependent types   Sergei Meshveliani
• [Agda] congruence on dependent types   Andreas Abel
• [Agda] congruence on dependent types   Nils Anders Danielsson
• [Agda] The HoTT book   Andrej Bauer
• [Agda] congruence on dependent types   Dominique Devriese
• [Agda] congruence on dependent types   Sergei Meshveliani
• [Agda] congruence on dependent types   Sergei Meshveliani
• [Agda] congruence on dependent types   Guillaume Brunerie
• [Agda] congruence on dependent types   Sergei Meshveliani
• [Agda] Re: [Coq-Club] The HoTT book   Victor Porton
• [Agda] Re: [Coq-Club] The HoTT book   Guillaume Brunerie
• [Agda] Performance improvements (Agda devel)   Andreas Abel
• [Agda] Performance improvements (Agda devel)   Sergei Meshveliani
• [Agda] congruence on dependent types   Nils Anders Danielsson
• [Agda] Performance improvements (Agda devel)   Wolfram Kahl
• [Agda] More universe polymorphism   Guillaume Brunerie
• [Agda] More universe polymorphism   Andreas Abel
• [Agda] Interesting issue with termination checker   Tom Cumming
• [Agda] More universe polymorphism   Guillaume Brunerie
• [Agda] More universe polymorphism   Darryl McAdams
• [Agda] Interesting issue with termination checker   Andreas Abel
• [Agda] Interesting issue with termination checker   Andreas Abel
• [Agda] More universe polymorphism   Nils Anders Danielsson
• [Agda] More universe polymorphism   Martin Escardo
• [Agda] More universe polymorphism   Dan Doel
• [Agda] More universe polymorphism   Martin Escardo
• [Agda] More universe polymorphism   Martin Escardo
• [Agda] More universe polymorphism   Guillaume Brunerie
• [Agda] More universe polymorphism   Martin Escardo
• [Agda] More universe polymorphism   Dan Doel
• [Agda] More universe polymorphism   Guillaume Brunerie
• [Agda] More universe polymorphism   Dan Doel
• [Agda] More universe polymorphism   Martin Escardo
• [Agda] More universe polymorphism   Guillaume Brunerie
• [Agda] More universe polymorphism   Gabriel Scherer
• [Agda] More universe polymorphism   Darryl McAdams
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Darryl McAdams
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Guillaume Brunerie
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Guillaume Brunerie
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Darryl McAdams
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Guillaume Brunerie
• [Agda] Numerical Programming in Agda   david rush
• [Agda] type/set nomenclature   James Cranch
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Martin Escardo
• [Agda] type/set nomenclature   Guillaume Brunerie
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Guillaume Brunerie
• [Agda] Devel: How to get back normalisation instead of simplification?   Wolfram Kahl
• [Agda] Devel: How to get back normalisation instead of simplification?   Guillaume Brunerie
• [Agda] type/set nomenclature   Andreas Abel
• [Agda] Numerical Programming in Agda   Andreas Abel
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Peter Hancock
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Darryl McAdams
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Guillaume Brunerie
• [Agda] import Data.Maybe.Core X import Data.Maybe   Carlos Camarao
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Peter Hancock
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Guillaume Brunerie
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Darryl McAdams
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Darryl McAdams
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Darryl McAdams
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Martin Escardo
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Guillaume Brunerie
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Guillaume Brunerie
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Martin Escardo
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Guillaume Brunerie
• Ambiguous constructors [Re: [Agda] import Data.Maybe.Core X import Data.Maybe]   Andreas Abel
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Bas Spitters
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Matthieu Sozeau
• Ambiguous constructors [Re: [Agda] import Data.Maybe.Core X import Data.Maybe]   Carlos Camarao
• [Agda] Termination checking, if-then-else X with   Carlos Camarao
• [Agda] successor / predecessor definition rejected for a tree-based natural number type   Paul Tarau
• [Agda] successor / predecessor definition rejected for a tree-based natural number type   Andrés Sicard-Ramírez
• [Agda] import Data.Maybe.Core X import Data.Maybe   Nils Anders Danielsson
• [Agda] More universe polymorphism   Martin Escardo
• [Agda] Termination checking, if-then-else X with   Andreas Abel
• [Agda] Termination-check doesn't know which case it should check?   Darryl McAdams
• [Agda] Termination-check doesn't know which case it should check?   Andrés Sicard-Ramírez
• [Agda] Termination-check doesn't know which case it should check?   Darryl McAdams
• [Agda] Termination checking, if-then-else X with   Carlos Camarao
• [Agda] Termination checking, if-then-else X with   Carlos Camarao
• [Agda] Termination checking, if-then-else X with   Andreas Abel
• [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")   Andreas Abel
• [Agda] Termination checking, if-then-else X with   Carlos Camarao
• [Agda] Type Theory Makes Headlines ; -) [ACM TechNews, Monday, July 1, 2013]   Wolfram Kahl
• [Agda] Termination checking, if-then-else X with   Andreas Abel
• [Agda] another possible without-K problem   Jason Reed
• [Agda] Re: wait whaaat   Dan Licata
• [Agda] More universe polymorphism   Dan Licata
• [Agda] More universe polymorphism   Martin Escardo
• [Agda] 2 PhD students, dependent types/functional programming, Chalmers   Nils Anders Danielsson
• [Agda] Re: wait whaaat   Nils Anders Danielsson
• [Agda] More universe polymorphism   Martin Escardo
• [Agda] More universe polymorphism   Martin Escardo
• [Agda] another possible without-K problem   Altenkirch Thorsten
• [Agda] another possible without-K problem   Andreas Abel
• [Agda] another possible without-K problem   Altenkirch Thorsten
• [Agda] another possible without-K problem   Dan Licata
• [Agda] another possible without-K problem   Dan Licata
• [Agda] another possible without-K problem   Altenkirch Thorsten
• [Agda] another possible without-K problem   Jason Reed
• [Agda] another possible without-K problem   drl at cs.cmu.edu
• Phantom arguments in functions [Re: [Agda] another possible without-K problem]   Andreas Abel
• [Agda] another possible without-K problem   Andreas Abel
• [Agda] another possible without-K problem   Dan Doel
• [Agda] another possible without-K problem   Andreas Abel
• [Agda] another possible without-K problem   drl at cs.cmu.edu
• Phantom arguments in functions [Re: [Agda] another possible without-K problem]   Guillaume Brunerie
• Phantom arguments in functions [Re: [Agda] another possible without-K problem]   Dan Licata
• Phantom arguments in functions [Re: [Agda] another possible without-K problem]   Martin Escardo
• [Agda] another possible without-K problem   Dan Licata
• [Agda] another possible without-K problem   Dan Doel
• [Agda] Question on the Agda tutorial   david rush
• [Agda] Re: Question on the Agda tutorial   Timon Gehr
• [Agda] Question on the Agda tutorial   Andrés Sicard-Ramírez
• Phantom arguments in functions [Re: [Agda] another possible without-K problem]   Andreas Abel
• Phantom arguments in functions [Re: [Agda] another possible without-K problem]   Guillaume Brunerie
• [Agda] MCS: Formal Proofs for Mathematics and Computer Science [Second Call for Papers]   Laurent Théry
• [Agda] Re: Question on the Agda tutorial   david rush
• [Agda] Homotopy Type Theory IRC Channel   Darin Morrison
• [Agda] Warning: hashable-1.2.0.x has serious performance bugs   Andreas Abel
• [Agda] Warning: hashable-1.2.0.x has serious performance bugs   Martin Escardo
• [Agda] Warning: hashable-1.2.0.x has serious performance bugs   Andreas Abel
• [Agda] Warning: hashable-1.2.0.x has serious performance bugs   Martin Escardo
• [Agda] Warning: hashable-1.2.0.x has serious performance bugs   Felipe Almeida Lessa
• [Agda] Warning: hashable-1.2.0.x has serious performance bugs   Andreas Abel
• [Agda] Warning: hashable-1.2.0.x has serious performance bugs   Felipe Almeida Lessa
• [Agda] Warning: hashable-1.2.0.x has serious performance bugs   Felipe Almeida Lessa
• [Agda] Warning: hashable-1.2.0.x has serious performance bugs   Andreas Abel
• [Agda] Warning: hashable-1.2.0.x has serious performance bugs   Felipe Almeida Lessa
• I accidentially [Re: [Agda] Warning: hashable-1.2.0.x has serious performance bugs]   Andreas Abel
• [Agda] DTP 2013 Call for Presentations   Stephanie Weirich
• [Agda] Call for Papers IFL 2013   publicityifl at gmail.com
• [Agda] Call for Papers PEPM 2014   publicityifl at gmail.com
• [Agda] Postdoc or research programmers, Maynooth, Co. Kildare Ireland   david rush
• [Agda] Type rather than Set   Sergei Meshveliani
• [Agda] Image f   Sergei Meshveliani
• [Agda] Agda Implementors' Meeting XVIII   Nils Anders Danielsson
• [Agda] Agda Implementors' Meeting XVIII   Guillaume Brunerie
• [Agda] Are there unicorns in Agda?   Maga Xalgverdiyev
• [Agda] Agda Implementors' Meeting XVIII   Andreas Abel
• [Agda] Insightful let's and where's   Darryl McAdams
• [Agda] Insightful let's and where's   Guillaume Brunerie
• [Agda] Re: Insightful let's and where's   Francesco Mazzoli
• [Agda] Re: Insightful let's and where's   Guillaume Brunerie
• [Agda] Re: Insightful let's and where's   Francesco Mazzoli
• [Agda] Re: Insightful let's and where's   Darryl McAdams
• [Agda] Lecturer/Senior Lecturer   Conor McBride
• [Agda] Strathclyde: Lecturer/Senior Lecturer   Conor McBride
• [Agda] extending equality   Sergei Meshveliani
• [Agda] extending equality   Matus Tejiscak
• [Agda] extending equality   Sergei Meshveliani
• [Agda] extending equality   Matus Tejiscak
• [Agda] hidden proofs   Sergei Meshveliani
• [Agda] hidden proofs   Liam O'Connor
• [Agda] hidden proofs   Sergei Meshveliani
• [Agda] hidden proofs   Wojciech Jedynak
• [Agda] extending setoid   Sergei Meshveliani
• [Agda] CRM conference "Type Theory, Homotopy Theory and Univalent Foundations" (call for participation)   Nicola Gambino
• [Agda] extending setoid   Andreas Abel
• [Agda] Call for Participation: HOPE 2013 (with special session in memory of John Reynolds)   Hongseok Yang
• [Agda] extending setoid   Sergei Meshveliani
• [Agda] extending setoid   Nils Anders Danielsson
• [Agda] 2nd CFP Post-proceedings TYPES 2013 Types for Proofs and Programs (open call)   Aleksy Schubert
• [Agda] Re: extending setoid   Sergei Meshveliani
• [Agda] tuple selectors   Sergei Meshveliani
• [Agda] tuple selectors   Andreas Abel
• [Agda] More universe polymorphism   Martin Escardo
• [Agda] CFP: PLPV 2014, Programming Languages meets Program Verification   Nils Anders Danielsson
• [Agda] tuple selectors   Darryl McAdams
• [Agda] question on `Any'   Sergei Meshveliani
• [Agda] question on `Any'   Dominique Devriese
• [Agda] Open modules and hard to predict normal forms   Andrea Vezzosi
• [Agda] Open modules and hard to predict normal forms   Andreas Abel
• [Agda] Open modules and hard to predict normal forms   Andrea Vezzosi
• [Agda] elem x (filter xs)   Sergei Meshveliani
• [Agda] elem x (filter xs)   Andrea Vezzosi
• [Agda] Running Agda on ARM   Wojciech Meyer
• [Agda] stack overflow in Agda 2.3.2.1   James Cranch
• [Agda] stack overflow in Agda 2.3.2.1   Andrés Sicard-Ramírez
• [Agda] stack overflow in Agda 2.3.2.1   Fredrik Nordvall Forsberg
• [Agda] Running Agda on ARM   Wojciech Meyer
• [Agda] stack overflow in Agda 2.3.2.1   Sergei Meshveliani
• [Agda] Re: Running Agda on ARM   Stefan Monnier
• [Agda] Re: Running Agda on ARM   Wojciech Meyer
• [Agda] `let postulate ... in'   Sergei Meshveliani
• [Agda] `let postulate ... in'   Andreas Abel
• [Agda] Call for participation IFL 2013   publicityifl at gmail.com
• [Agda] [TYPES/announce] ICFP 2013 Call for Participation   Tarmo Uustalu
• [Agda] Why is propositional equality "Set a" instead of just Set?   Jonathan Leivent
• [Agda] Why is propositional equality "Set a" instead of just Set?   Wolfram Kahl
• [Agda] question on `Any'   Sergei Meshveliani
• [Agda] x \in (gfilter _ ys)   Sergei Meshveliani
• [Agda] Why is propositional equality "Set a" instead of just Set?   Jonathan Leivent
• [Agda] question on `Any'   Dominique Devriese
• [Agda] Why is propositional equality "Set a" instead of just Set?   Andreas Abel
• [Agda] Why is propositional equality "Set a" instead of just Set?   Dan Licata
• [Agda] Why is propositional equality "Set a" instead of just Set?   Conor McBride
• [Agda] Why is propositional equality "Set a" instead of just Set?   Jonathan Leivent
• [Agda] certain report   Sergei Meshveliani
• [Agda] Why is propositional equality "Set a" instead of just Set?   Martin Escardo
• [Agda] Why is propositional equality "Set a" instead of just Set?   Wolfram Kahl
• [Agda] Why is propositional equality "Set a" instead of just Set?   Martin Escardo
• [Agda] Why is propositional equality "Set a" instead of just Set?   Jonathan Leivent
• [Agda] Why is propositional equality "Set a" instead of just Set?   Nils Anders Danielsson
• [Agda] question on `Any'   Nils Anders Danielsson
• [Agda] Running Agda on ARM   Nils Anders Danielsson
• [Agda] certain report   Andreas Abel
• [Agda] AIM XVIII: Call for participation   Guilhem Moulin
• [Agda] Running Agda on ARM   Wojciech Meyer
• [Agda] certain report   Sergei Meshveliani
• [Agda] Why is propositional equality "Set a" instead of just Set?   Jonathan Leivent
• [Agda] Why is propositional equality "Set a" instead of just Set?   Nils Anders Danielsson
• [Agda] Why is propositional equality "Set a" instead of just Set?   Conor McBride
• [Agda] Why is propositional equality "Set a" instead of just Set?   Nils Anders Danielsson
• [Agda] Re: extending setoid   Nils Anders Danielsson
• [Agda] Why is propositional equality "Set a" instead of just Set?   Jonathan Leivent
• Phantom arguments in functions [Re: [Agda] another possible without-K problem]   Nils Anders Danielsson
• [Agda] MCS: Formal Proofs for Mathematics and Computer Science [Last Call for Papers]   Laurent Théry
• [Agda] Why is propositional equality "Set a" instead of just Set?   Nils Anders Danielsson
• [Agda] Second call for papers for PEPM 2014   planpublicity at gmail.com
• [Agda] Why is propositional equality "Set a" instead of just Set?   Martin Escardo
• [Agda] Why is propositional equality "Set a" instead of just Set?   Nils Anders Danielsson
• [Agda] Perplexed by compile behavior   Chris Moline
• [Agda] another possible without-K problem   Nils Anders Danielsson
• [Agda] Why is propositional equality "Set a" instead of just Set?   Dan Licata
• [Agda] another possible without-K problem   Bas Spitters
• [Agda] Perplexed by compile behavior   Nils Anders Danielsson
• [Agda] debian agda popularity   Peter Divianszky
• [Agda] How do I handle haskell type contexts from agda when using the ffi?   Chris Moline
• [Agda] Re: How do I handle haskell type contexts from agda when using the ffi?   Chris Moline
• [Agda] underscore in \neg   Sergei Meshveliani
• [Agda] underscore in \neg   Matus Tejiscak
• [Agda] underscore in \neg   Wojciech Jedynak
• [Agda] rewriting product types vs. single ctor data/record types   Jonathan Leivent
• [Agda] rewriting product types vs. single ctor data/record types   Darryl McAdams
• [Agda] CIE 2014: Language, Life, Limits. June 23-27, 2014, Budapest. Preliminary Announcement.   S B Cooper
• [Agda] again `with' vs `case'   Sergei Meshveliani
• [Agda] How do I handle haskell type contexts from agda when using the ffi?   Nils Anders Danielsson
• [Agda] rewriting product types vs. single ctor data/record types   Nils Anders Danielsson
• [Agda] again `with' vs `case'   Nils Anders Danielsson
• [Agda] rewriting product types vs. single ctor data/record types   Jason Gross
• [Agda] again `with' vs `case'   Sergei Meshveliani
• [Agda] [REMINDER] AIM XVIII: Call for participation   Guilhem Moulin
• [Agda] repeated Level.suc   Sergei Meshveliani
• [Agda] Closed Predicate f in lib07   Sergei Meshveliani
• [Agda] Closed Predicate f in lib07   Arseniy Alekseyev
• [Agda] Closed Predicate f in lib07   Sergei Meshveliani
• [Agda] Closed Predicate f in lib07   Sergei Meshveliani
• [Agda] Level symbols   Sergei Meshveliani
• [Agda] Closed Predicate f in lib07   Arseniy Alekseyev
• [Agda] Level symbols   Wolfram Kahl
• [Agda] Coq-related postdoc position at Inria-Saclay   Bruno Barras
• [Agda] Windows/Linux versions of Agda   Aaron Stump
• [Agda] Windows/Linux versions of Agda   Jason Dagit
• [Agda] Windows/Linux versions of Agda   Aaron Stump
• [Agda] Windows/Linux versions of Agda   Jason Dagit
• [Agda] Windows/Linux versions of Agda   Aaron Stump
• [Agda] Windows/Linux versions of Agda   Martin Escardo
• [Agda] Windows/Linux versions of Agda   Sam Staton
• [Agda] Windows/Linux versions of Agda   Andrew Pitts
• [Agda] Windows/Linux versions of Agda   Martin Escardo
• [Agda] Open PhD Position at DemTech/IT University of Copenhagen   Carsten Schürmann
• [Agda] again `with' vs `case'   Nils Anders Danielsson
• [Agda] Windows/Linux versions of Agda   Nils Anders Danielsson
• [Agda] Windows/Linux versions of Agda   Aaron Stump
• [Agda] Windows/Linux versions of Agda   Dan Licata
• [Agda] Windows/Linux versions of Agda   Aaron Stump
• [Agda] Windows/Linux versions of Agda   Dan Licata
• [Agda] Windows/Linux versions of Agda   Aaron Stump
• [Agda] Circular proof causes stack overflow   Dan Piponi
• [Agda] Circular proof causes stack overflow   Wojciech Meyer
• [Agda] Circular proof causes stack overflow   Dan Piponi
• [Agda] Circular proof causes stack overflow   Wojciech Meyer
• [Agda] Circular proof causes stack overflow   Dan Doel
• [Agda] Circular proof causes stack overflow   Dan Piponi
• [Agda] Circular proof causes stack overflow   Nils Anders Danielsson
• [Agda] Final CFP Post-proceedings TYPES 2013 Types for Proofs and Programs (open call)   Aleksy Schubert
• [Agda] Oberwolfach Seminar on Mathematics for Scientific Programming   Jeremy.Gibbons at cs.ox.ac.uk
• [Agda] Circular proof causes stack overflow   Andreas Abel
• [Agda] VMCAI 2014 DEADLINE EXTENSION   Xavier Rival
• [Agda] HOPE 2013 Last Call for Participation (with Workshop Program)   Hongseok Yang
• [Agda] Solving Presburger arithmetic goals   Rodrigo Ribeiro
• [Agda] Solving Presburger arithmetic goals   Dr. ÉRDI Gergő
• [Agda] Solving Presburger arithmetic goals   Dr. ÉRDI Gergő
• [Agda] APLAS 2013 - Call for Posters and Demos   Shin-ya Katsumata
• [Agda] CSL-LICS 2014 - First Call for Papers   Andrzej Murawski
• [Agda] "Semantics of proofs and certified mathematics", IHP trimester, Paris, spring 2014: final call for financial support requests (deadline Sep 23th)   Hugo Herbelin
• [Agda] Re: [Coq-Club] "Semantics of proofs and certified mathematics", IHP trimester, Paris, spring 2014: final call for financial support requests (deadline Sep 23th)   Pierre Courtieu
• [Agda] FLoC Final Call for Workshops (The Sixth Federated Logic Conference, July 2014, Vienna)   David Pichardie
• [Agda] Final Call for Workshop Proposals   Georg Moser
• [Agda] meta vars regression from version 2.3.2   Christian Sattler
• [Agda] max (x :: xs)   Serge D. Mechveliani
• [Agda] Preorder.setoid ?   Sergei Meshveliani
• [Agda] Preorder.setoid ?   Nils Anders Danielsson
• [Agda] max (x :: xs)   Nils Anders Danielsson
• [Agda] meta vars regression from version 2.3.2   Nils Anders Danielsson
• [Agda] Preorder.setoid ?   Sergei Meshveliani
• [Agda] Re: Issue 897 in agda: unnatural space behavoir of the checker   Sergei Meshveliani
• [Agda] Final CFP for PEPM 2014   planpublicity at gmail.com
• [Agda] Re: Issue 897 in agda: unnatural space behavoir of the checker   Nils Anders Danielsson
• [Agda] Unification of function types   Jesper Cockx
• [Agda] Unification of function types   Nils Anders Danielsson
• [Agda] Re: Issue 897 in agda: unnatural space behavoir of the checker   Sergei Meshveliani
• [Agda] Unification of function types   Jesper Cockx
• [Agda] Re: Issue 897 in agda: unnatural space behavoir of the checker   Nils Anders Danielsson
• [Agda] guardedness-preserving-type-constructors failing termination checker   Twan van Laarhoven
• [Agda] guardedness-preserving-type-constructors failing termination checker   Nils Anders Danielsson
• [Agda] I'm having an issue modeling type classes with records   Chris Moline
• case or with [Re: [Agda] Re: Issue 897 in agda: unnatural space behavoir of the checker]   Andreas Abel
• [Agda] I'm having an issue modeling type classes with records   Andreas Abel
• [Agda] Unification of function types   Andreas Abel
• [Agda] guardedness-preserving-type-constructors failing termination checker   Andreas Abel
• [Agda] Unification of function types   Vilhelm Sjöberg
• [Agda] Unification of function types   Guillaume Brunerie
• [Agda] Unification of function types   Jesper Cockx
• [Agda] Nat.DivMod details in lib-0.7   Sergei Meshveliani
• [Agda] suc _ > 0   Sergei Meshveliani
• [Agda] _<=_ and _<_   Sergei Meshveliani
• [Agda] stdlib for practical programming   Dmytro Starosud
• [Agda] stdlib for practical programming   Sergei Meshveliani
• [Agda] _<=_ and _<_   Sergei Meshveliani
• [Agda] stdlib for practical programming   Mianlai Zhou
• [Agda] stdlib for practical programming   Sergei Meshveliani
• [Agda] _<=_ and _<_   Sergei Meshveliani
• [Agda] _<=_ and _<_   Sergei Meshveliani
• [Agda] _<=_ and _<_   Sergei Meshveliani
• [Agda] stdlib for practical programming   Dmytro Starosud
• [Agda] stdlib for practical programming   Sergei Meshveliani
• [Agda] stdlib for practical programming   Paolo Capriotti
• [Agda] stdlib for practical programming   Sergei Meshveliani
• [Agda] stdlib for practical programming   Dmytro Starosud
• [Agda] stdlib for practical programming   Sergei Meshveliani
• [Agda] `with' --> `case' fails   Sergei Meshveliani
• [Agda] stdlib for practical programming   Dmytro Starosud
• [Agda] stdlib for practical programming   Wolfram Kahl
• [Agda] stdlib for practical programming   Sergei Meshveliani
• [Agda] `with' --> `case' fails   Andreas Abel
• [Agda] stdlib for practical programming   Dmytro Starosud
• [Agda] stdlib for practical programming   Andreas Abel
• [Agda] stdlib for practical programming   Dmytro Starosud
• [Agda] `with' --> `case' fails   Sergei Meshveliani
• [Agda] Windows/Linux versions of Agda   Nils Anders Danielsson
• [Agda] stdlib for practical programming   Sergei Meshveliani
• [Agda] add <-antysym to IsStrictPatialOrder ?   Sergei Meshveliani
• [Agda] termination example   Serge D. Mechveliani
• [Agda] termination example   Andreas Abel
• [Agda] Using instance arguments for pointed types   Guillaume Brunerie
• [Agda] Using instance arguments for pointed types   Jesper Cockx
• [Agda] 2nd CFP: PLPV 2014, Programming Languages meets Program Verification   Nils Anders Danielsson
• [Agda] Using instance arguments for pointed types   Dmytro Starosud
• [Agda] Using instance arguments for pointed types   Guillaume Brunerie
• Fwd: [Agda] Using instance arguments for pointed types   Matteo Acerbi
• [Agda] Using instance arguments for pointed types   Guillaume Brunerie
• [Agda] Recursive instance search limited in depth   Guillaume Brunerie
• [Agda] Recursive instance search limited in depth   Dominique Devriese
• [Agda] Recursive instance search limited in depth   Dominique Devriese
• [Agda] Recursive instance search limited in depth   Dmytro Starosud
• [Agda] Recursive instance search limited in depth   Edward Kmett
• [Agda] Recursive instance search limited in depth   Dominique Devriese
• [Agda] Re: Agda Digest, Vol 98, Issue 3   David Darais
• [Agda] 2nd CfP (deadline 31 Oct) Math. in Comp. Sci. Special Issue 'Enabling Domain Experts to use Formalised Reasoning'   Christoph LANGE
• [Agda] Agda Digest, Vol 98, Issue 3   Matthieu Sozeau
• [Agda] Agda Digest, Vol 98, Issue 3   Dominique Devriese
• [Agda] Inference for invariant arguments question   Andrea Vezzosi
• [Agda] Exports example? Making ADT constructors private?   Evan Czaplicki
• [Agda] Exports example? Making ADT constructors private?   Brian McKenna
• [Agda] using Induction.Nat   Sergei Meshveliani
• [Agda] using Induction.Nat   Daniel Peebles
• [Agda] 2nd CfP: Relational and Algebraic Methods in Computer Science (RAMiCS 2014)   Peter Höfner
• [Agda] using Induction.Nat   Andreas Abel
• [Agda] using Induction.Nat   Sergei Meshveliani
• [Agda] "Semantics of proofs and certified mathematics", IHP trimester, Paris, spring 2014: call for starting school application and workshop registration   Hugo Herbelin
• [Agda] Exports example? Making ADT constructors private?   Evan Czaplicki
• [Agda] ordering uniqueness   Marco Maggesi
• [Agda] using Induction.Nat   Andreas Abel
• [Agda] ordering uniqueness   Sergei Meshveliani
• [Agda] ordering uniqueness   Twan van Laarhoven
• [Agda] strange termination check   Sergei Meshveliani
• [Agda] strange termination check   Sergei Meshveliani
• [Agda] ordering uniqueness   Marco Maggesi
• [Agda] ordering uniqueness   Marco Maggesi
• [Agda] suc suc _ : Bit   Sergei Meshveliani
• [Agda] suc suc _ : Bit   Andreas Abel
• [Agda] strange termination check   Andreas Abel
• [Agda] strange termination check   Sergei Meshveliani
• [Agda] strange termination check   Sergei Meshveliani
• [Agda] matching to Sum   Sergei Meshveliani
• [Agda] Argument order, universes and erasability   Mathijs Kwik
• [Agda] Argument order, universes and erasability   Dan Doel
• [Agda] Call for Talk Proposals: Data-Centric Programming, San Diego, Jan 2014   Jeremy.Gibbons at cs.ox.ac.uk
• [Agda] Argument order, universes and erasability   gallais
• [Agda] Argument order, universes and erasability   Pierre-Evariste Dagand
• [Agda] import in st.library   Sergei Meshveliani
• [Agda] import in st.library   Wojciech Jedynak
• [Agda] Argument order, universes and erasability   Andreas Abel
• [Agda] matching to Sum   Andreas Abel
• [Agda] Argument order, universes and erasability   Nils Anders Danielsson
• [Agda] strange termination check   Nils Anders Danielsson
• [Agda] Exports example? Making ADT constructors private?   Nils Anders Danielsson
• [Agda] matching to Sum   Sergei Meshveliani
• [Agda] matching to Sum   Andreas Abel
• [Agda] fromJ ∘ toJ level   Sergei Meshveliani
• [Agda] CFP for MSFP 2014   Neelakantan Krishnaswami
• [Agda] fromJ ∘ toJ level   Twan van Laarhoven
• [Agda] Argument order, universes and erasability   wren at freegeek.org
• [Agda] ≡ → ≈   Sergei Meshveliani
• [Agda] ≡ → ≈   Twan van Laarhoven
• [Agda] ≡ → ≈   Matus Tejiscak
• [Agda] ≡ → ≈   Wolfram Kahl
• [Agda] TAMC2014 in Chennai, India, April 11-13, 2014   S B Cooper
• [Agda] Windows/Linux versions of Agda   Nils Anders Danielsson
• [Agda] Modelling term-rewriting systems in Agda   Jacques Carette
• [Agda] Modelling term-rewriting systems in Agda   Sergei Meshveliani
• [Agda] Modelling term-rewriting systems in Agda   Sergei Meshveliani
• [Agda] Modelling term-rewriting systems in Agda   Jacques Carette
• [Agda] Modelling term-rewriting systems in Agda   Jacques Carette
• [Agda] Agda compiler optimizations   agda newb
• [Agda] Modelling term-rewriting systems in Agda   Sergei Meshveliani
• [Agda] Modelling term-rewriting systems in Agda   Jacques Carette
• [Agda] Modelling term-rewriting systems in Agda   Sergei Meshveliani
• [Agda] Modelling term-rewriting systems in Agda   Twan van Laarhoven
• [Agda] Modelling term-rewriting systems in Agda   Jacques Carette
• [Agda] Modelling term-rewriting systems in Agda   Aaron Stump
• [Agda] Modelling term-rewriting systems in Agda   Peter Hancock
• [Agda] Agda compiler optimizations   Andreas Abel
• [Agda] Inference for invariant arguments question   Andreas Abel
• [Agda] Modelling term-rewriting systems in Agda   Christian Sternagel
• [Agda] Modelling term-rewriting systems in Agda   Twan van Laarhoven
• [Agda] All P xs -> x in xs -> ..   Sergei Meshveliani
• [Agda] All P xs -> x in xs -> ..   Nils Anders Danielsson
• [Agda] _iff_ in lib   Sergei Meshveliani
• [Agda] _iff_ in lib   Nils Anders Danielsson
• [Agda] not-all -> any-not   Sergei Meshveliani
• [Agda] not-all -> any-not   Jesper Cockx
• [Agda] Function.Equivalence._⇔_   Sergei Meshveliani
• Re: [Agda] Function.Equivalence._⇔_   Andrés Sicard-Ramírez
• [Agda] _iff_ in lib   Andreas Abel
• Re: [Agda] Function.Equivalence._⇔_   Nicolas Pouillard
• [Agda] Function.Equivalence._⇔_   Nils Anders Danielsson
• [Agda] Function.Equivalence._⇔_   Martin Escardo
• [Agda] Function.Equivalence._⇔_   Nils Anders Danielsson
• Re: [Agda] Function.Equivalence._⇔_   Altenkirch Thorsten
• [Agda] Function.Equivalence._⇔_   Sergei Meshveliani
• [Agda] strange `case' requirement   Sergei Meshveliani
• [Agda] strange `case' requirement   Wolfram Kahl
• [Agda] strange `case' requirement   Sergei Meshveliani
• [Agda] Relational & Algebraic Methods --- RAMiCS 2014 --- Final CFP, with Deadlines extended!   Wolfram Kahl
• [Agda] Nat -iso- Bin   Sergei Meshveliani
• [Agda] Nat -iso- Bin   Sergei Meshveliani
• [Agda] Nat -iso- Bin   Sergei Meshveliani
• [Agda] Nat -iso- Bin   Arseniy Alekseyev
• [Agda] How to cite Agda?   Cai
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] Termination problems with "with" and recursion   Jesper Cockx
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] Termination problems with "with" and recursion   Jesper Cockx
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] Termination problems with "with" and recursion   Dominique Devriese
• [Agda] Nat -iso- Bin   Nils Anders Danielsson
• [Agda] ANNOUNCE: Agda 2.3.2.2   Nils Anders Danielsson
• [Agda] ICFP 2014: Call for Workshop & Co-located Even Proposals   David Van Horn
• [Agda] ICFP 2014: Call for Workshop & Co-located Event Proposals   David Van Horn
• [Agda] Termination problems with "with" and recursion   Andreas Abel
• [Agda] Termination problems with "with" and recursion   Dominique Devriese
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] ANNOUNCE: Agda 2.3.2.2   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.3.2.2   Nils Anders Danielsson
• [Agda] Joint 25th RTA & 12th TLCA: CALL FOR PAPERS   Luca Paolini
• [Agda] Proving m + (1 + n) == 1 + (m + n)   Jan Stolarek
• [Agda] Proving m + (1 + n) == 1 + (m + n)   Twan van Laarhoven
• [Agda] HCAR report   Andreas Abel
• [Agda] HCAR report (without the PDF)   Andreas Abel
• [Agda] ANNOUNCE: Agda 2.3.2.2   Joachim Breitner
• [Agda] lectureships at Imperial, including in verification   Gardner, Philippa A
• [Agda] ANNOUNCE: Agda 2.3.2.2   Nils Anders Danielsson
• [Agda] ANNOUNCE: Agda 2.3.2.2   Andreas Abel
• [Agda] ANNOUNCE: Agda 2.3.2.2   Joachim Breitner
• [Agda] "metavariable" message   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.3.2.2   Andreas Abel
• [Agda] "metavariable" message   Andreas Abel
• [Agda] ANNOUNCE: Agda 2.3.2.2   Joachim Breitner
• [Agda] ANNOUNCE: Agda 2.3.2.2   Andreas Abel
• [Agda] ANNOUNCE: Agda 2.3.2.2   Joachim Breitner
• [Agda] Proving m + (1 + n) == 1 + (m + n)   Jan Stolarek
• [Agda] Re: Nat -iso- Bin   Sergei Meshveliani
• [Agda] Recursive instance search limited in depth   Andreas Abel
• [Agda] Recursive instance search limited in depth   Nils Anders Danielsson
• [Agda] add <-antysym to IsStrictPatialOrder ?   Nils Anders Danielsson
• [Agda] pair list in lib ?   Sergei Meshveliani
• [Agda] pair list in lib ?   Twan van Laarhoven
• [Agda] pair list in lib ?   Twan van Laarhoven
• [Agda] pair list in lib ?   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.3.2.2   Nils Anders Danielsson
• [Agda] ANNOUNCE: Agda 2.3.2.2   Joachim Breitner
• [Agda] ANNOUNCE: Agda 2.3.2.2   Andreas Abel
• [Agda] Agda bug   Carlos Camarao
• [Agda] Agda bug   Wolfram Kahl
• [Agda] Agda bug   Sergei Meshveliani
• [Agda] Agda bug   Carlos Camarao
• [Agda] Agda bug   Carlos Camarao
• [Agda] Dev. version woes -- Agda/Prim.agda   Jacques Carette
• [Agda] Dev. version woes -- Agda/Prim.agda   gallais
• [Agda] Agda bug   Ulf Norell
• [Agda] Agda bug   Nils Anders Danielsson
• [Agda] Agda bug   Carlos Camarao
• [Agda] Agda bug   Nils Anders Danielsson
• [Agda] Dev. version woes -- Agda/Prim.agda   Jacques Carette
• [Agda] Agda bug   Carlos Camarao
• [Agda] Call for Workshops: Conf. Intelligent Computer Mathematics (CICM 2014)   Serge Autexier
• [Agda] case ((a , b) , (c , d))   Sergei Meshveliani
• [Agda] case ((a , b) , (c , d))   Nils Anders Danielsson
• [Agda] LaTeX-Backend: \renewcommand{\defaultcolumn}{...} shows no effect   Andreas Abel
• [Agda] LaTeX-Backend: \renewcommand{\defaultcolumn}{...} shows no effect   Alan Jeffrey
• [Agda] LaTeX-Backend: \renewcommand{\defaultcolumn}{...} shows no effect   Andreas Abel
• [Agda] Re: LaTeX-Backend: \renewcommand{\defaultcolumn}{...} shows no effect   Stevan Andjelkovic
• [Agda] Proving a + suc b == b + suc a   Jan Stolarek
• [Agda] Proving a + suc b == b + suc a   Martin Escardo
• [Agda] Proving a + suc b == b + suc a   Andrea Vezzosi
• [Agda] Proving a + suc b == b + suc a   Jan Stolarek
• [Agda] Proving a + suc b == b + suc a   Jan Stolarek
• [Agda] Proving a + suc b == b + suc a   Mateusz Kowalczyk
• [Agda] Proving a + suc b == b + suc a   Serge D. Mechveliani
• [Agda] Proving a + suc b == b + suc a   Jan Stolarek
• [Agda] Sign.+ ◃   Sergei Meshveliani
• [Agda] Proving a + suc b == b + suc a   Nils Anders Danielsson
• [Agda] Level constraints   Christian Sattler
• [Agda] Level constraints   Nils Anders Danielsson
• [Agda] Sign.+ ◃   Nils Anders Danielsson
• [Agda] Level constraints   Martin Escardo
• [Agda] Level constraints   Nils Anders Danielsson
• [Agda] Level constraints   Martin Escardo
• [Agda] Level constraints   Martin Escardo
• [Agda] Level constraints   Martin Escardo
• [Agda] Level constraints   Martin Escardo
• [Agda] Level constraints   Nils Anders Danielsson
• [Agda] Level constraints   Matthieu Sozeau
• [Agda] Level constraints   Wolfram Kahl
• [Agda] Level constraints   Martin Escardo
• [Agda] Level constraints   Wolfram Kahl
• [Agda] "Semantics of Proofs and Certified Mathematics", IHP trimester (second call for starting school and workshop registration)   Hugo Herbelin
• [Agda] Agda implementation of McBride's unification paper?   Kenichi Asai
• [Agda] Agda implementation of McBride's unification paper?   Dr. ERDI Gergo
• [Agda] Agda implementation of McBride's unification paper?   Nils Anders Danielsson
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] Agda implementation of McBride's unification paper?   Pepijn Kokke
• [Agda] Termination problems with "with" and recursion   Andrea Vezzosi
• [Agda] Agda implementation of McBride's unification paper?   Andrea Vezzosi
• [Agda] CFP POPL Workshop on Data-Centric Programming (Extension)   Judith Bishop
• [Agda] Re: Relaxing the strict positivity requirement   Abhishek Anand
• [Agda] Termination problems with "with" and recursion   Nils Anders Danielsson
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] SR 2014 - call for contributions   murano
• [Agda] ACM SIGPLAN Workshop on Data-Centric Programming (at POPL) - talk proposal deadline extended to 22nd Nov   Jeremy.Gibbons at cs.ox.ac.uk
• [Agda] Call for participation: PLPV 2014   Nils Anders Danielsson
• [Agda] darcs - dev-version fail   Sergei Meshveliani
• [Agda] darcs - dev-version fail   Nils Anders Danielsson
• [Agda] darcs - dev-version fail   Ulf Norell
• [Agda] A different implementation of --without-K   Jesper Cockx
• [Agda] A different implementation of --without-K   Nils Anders Danielsson
• [Agda] A different implementation of --without-K   Pierre Boutillier
• [Agda] A different implementation of --without-K   Jesper Cockx
• [Agda] A different implementation of --without-K   Jesper Cockx
• [Agda] First Call for Papers: Conf. Intelligent Computer Mathematics (CICM 2014)   Serge Autexier
• [Agda] A different implementation of --without-K   Dan Licata
• [Agda] darcs-Nov2013 vs Agda-2.3.2.2   Sergei Meshveliani
• [Agda] Defining Coq(w/o Prop) in Agda using Induction Recursion   Abhishek Anand
• [Agda] Defining Coq(w/o Prop) in Agda using Induction Recursion   Nils Anders Danielsson
• [Agda] Development version of agda-mode doesn't recognize symlinks?   Jan Stolarek
• [Agda] Development version of agda-mode doesn't recognize symlinks?   Nils Anders Danielsson
• [Agda] Defining Coq(w/o Prop) in Agda using Induction Recursion   Peter Hancock
• [Agda] case...lambda   Sergei Meshveliani
• [Agda] ℕ <--iso--> Bin⁺ ∩ HasLast1if   Sergei Meshveliani
• [Agda] case...lambda   Daniel Peebles
• [Agda] Development version of agda-mode doesn't recognize symlinks?   Jan Stolarek
• [Agda] difficulties with patterns   Sergei Meshveliani
• [Agda] difficulties with patterns   Andreas Abel
• [Agda] If all functions (N->N)->N are continuous, then 0=1.   Martin Escardo
• [Agda] Showing Reflection.Name   Pepijn Kokke
• [Agda] Writing a paper in Literate Agda   Alan Jeffrey
• [Agda] If all functions (N->N)->N are continuous, then 0=1.   Altenkirch Thorsten
• [Agda] If all functions (N->N)->N are continuous, then 0=1.   Martin Escardo
• [Agda] Writing a paper in Literate Agda   Tillmann Rendel
• [Agda] If all functions (N->N)->N are continuous, then 0=1.   Martin Escardo
• [Agda] A different implementation of --without-K   Jesper Cockx
• [Agda] Writing a paper in Literate Agda   Alan Jeffrey
• [Agda] difficulties with patterns   Sergei Meshveliani
• [Agda] difficulties with patterns   Nils Anders Danielsson
• [Agda] If all functions (N->N)->N are continuous, then 0=1.   Altenkirch Thorsten
• [Agda] difficulties with patterns   Andreas Abel
• [Agda] A different implementation of --without-K   Andreas Abel
• [Agda] Writing a paper in Literate Agda   Abhishek Anand
• [Agda] Writing a paper in Literate Agda   Mateusz Kowalczyk
• [Agda] difficulties with patterns   Sergei Meshveliani
• [Agda] Writing a paper in Literate Agda   Nils Anders Danielsson
• [Agda] A different implementation of --without-K   Nils Anders Danielsson
• [Agda] Writing a paper in Literate Agda   Alan Jeffrey
• [Agda] A different implementation of --without-K   Harley D. Eades III
• [Agda] A different implementation of --without-K   Andreas Abel
• [Agda] A different implementation of --without-K   Altenkirch Thorsten
• [Agda] A different implementation of --without-K   Jason Gross
• [Agda] If all functions (N->N)->N are continuous, then 0=1.   Andrea Vezzosi
• [Agda] Development version of agda-mode doesn't recognize symlinks?   Andreas Abel
• [Agda] A different implementation of --without-K   Andreas Abel
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] Agda development   Jan Stolarek
• [Agda] Agda development   Nicolas Pouillard
• [Agda] Termination problems with "with" and recursion   Andreas Abel
• github? [Re: [Agda] Agda development]   Andreas Abel
• github? [Re: [Agda] Agda development]   Andrés Sicard-Ramírez
• github? [Re: [Agda] Agda development]   Wojciech Jedynak
• [Agda] A different implementation of --without-K   Martin Escardo
• [Agda] If all functions (N->N)->N are continuous, then 0=1.   Martin Escardo
• [Agda] Writing a paper in Literate Agda   Abhishek Anand
• [Agda] --html   Martin Escardo
• [Agda] --html   Ulf Norell
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• github? [Re: [Agda] Agda development]   Jan Stolarek
• github? [Re: [Agda] Agda development]   Ulf Norell
• github? [Re: [Agda] Agda development]   Jan Stolarek
• [Agda] AI4FM 2014: Call for Short Contributions   Iain Whiteside
• github? [Re: [Agda] Agda development]   Guillaume Brunerie
• github? [Re: [Agda] Agda development]   Ulf Norell
• [Agda] Termination problems with "with" and recursion   Andreas Abel
• [Agda] A different implementation of --without-K   Nils Anders Danielsson
• github? [Re: [Agda] Agda development]   Jan Stolarek
• github? [Re: [Agda] Agda development]   Guillaume Brunerie
• [Agda] A different implementation of --without-K   Bas Spitters
• [Agda] Writing a paper in Literate Agda   Nils Anders Danielsson
• [Agda] Termination problems with "with" and recursion   Nils Anders Danielsson
• [Agda] A different implementation of --without-K   Conor McBride
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] Termination problems with "with" and recursion   Andreas Abel
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• github? [Re: [Agda] Agda development]   Dan Doel
• [Agda] proofs for binary conversion   Sergei Meshveliani
• github? [Re: [Agda] Agda development]   Alan Jeffrey
• github? [Re: [Agda] Agda development]   Jan Stolarek
• [Agda] CSL-LICS 2014 - Call for Papers   Andrzej Murawski
• [Agda] PhD positions in Nottingham   Altenkirch Thorsten
• [Coq-Club] [Agda] Defining Coq(w/o Prop) in Agda using Induction Recursion   Edwin Westbrook
• [Coq-Club] [Agda] Defining Coq(w/o Prop) in Agda using Induction Recursion   Nils Anders Danielsson
• [Agda] [TFP 2014] 1st Call For Papers   Peter Achten
• [Agda] [TFP 2014] 1st Call For Papers   Peter Achten
• [Agda] Termination problems with "with" and recursion   Andreas Abel
• [Agda] If all functions (N->N)->N are continuous, then 0=1.   Andrea Vezzosi
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] Termination problems with "with" and recursion   Andreas Abel
• [Agda] common argument structure   Sergei Meshveliani
• [Agda] Recompilation triggers rechecking?   Andreas Abel
• [Agda] Recompilation triggers rechecking?   Andrea Vezzosi
• [Agda] Termination problems with "with" and recursion   Jan Stolarek
• [Agda] decidable _∈_   Sergei Meshveliani
• [Agda] decidable _∈_   Sergei Meshveliani
• [Agda] Recompilation triggers rechecking?   Andreas Abel
• [Agda] anonymous modules   Sergei Meshveliani
• [Agda] Recompilation triggers rechecking?   Nils Anders Danielsson
• [Agda] ITP 2015 - Call for Bids   Gerwin Klein
• [Agda] Bool P -> Dec P'   Sergei Meshveliani
• [Agda] Bool P -> Dec P'   Ulf Norell
• [Agda] Fully funded PhD studentships in Pervasive Parallelism at Edinburgh   James Cheney
• [Agda] How to case split on the value of a function (the second time)?   Jacques Carette
• [Agda] Recompilation triggers rechecking?   Andrea Vezzosi
• [Agda] How to case split on the value of a function (the second time)?   Andreas Abel
• [Agda] cancel-just-in≡   Sergei Meshveliani
• [Agda] cancel-just-in≡   Sergei Meshveliani
• [Agda] with -> case example   Sergei Meshveliani
• [Agda] with -> case example   Andreas Abel
• [Agda] How to case split on the value of a function (the second time)?   Nils Anders Danielsson
• [Agda] How to case split on the value of a function (the second time)?   Jacques Carette
• [Agda] Call for Participation PEPM 2014 (co-located with POPL 2014) === P E P M 2014 ===   planpublicity at gmail.com
• [Agda] Research Fellowship at Leeds   Nicola Gambino
• [Agda] unzip   Serge D. Mechveliani
• [Agda] (\ x , e → x ^ e)   Sergei Meshveliani
• [Agda] (\ x , e → x ^ e)   Matus Tejiscak
• [Agda] Classical Logic and Computation 2014 in Wien - First Call for Papers   Berardi Stefano
• [Agda] SSTiC 2014: December 21st, 1st registration deadline   GRLMC
• [Agda] finite map   Sergei Meshveliani
• [Agda] unsolved metas in Respects₂   Sergei Meshveliani
• [Agda] unsolved metas in Respects₂   Twan van Laarhoven
• [Agda] unsolved metas in Respects₂   Sergei Meshveliani
• [Agda] defining coinductive types   Aaron Stump
• [Agda] defining coinductive types   Andreas Abel
• [Agda] SBLP 2014 --- Call for Papers   Rodrigo Ribeiro
• [Agda] defining coinductive types   Aaron Stump
• [Agda] finite map   Sergei Meshveliani
• [Agda] defining coinductive types   Nils Anders Danielsson
• [Agda] defining coinductive types   Aaron Stump
• [Agda] defining coinductive types   Nils Anders Danielsson
• [Agda] defining coinductive types   Aaron Stump
• [Agda] x ∈ (append y xs) → ..   Sergei Meshveliani
• [Agda] defining coinductive types   Nils Anders Danielsson
• [Agda] defining coinductive types   Aaron Stump
• [Agda] Writing a paper in Literate Agda   Abhishek Anand
• [Agda] defining coinductive types   Wojciech Jedynak
• [Agda] defining coinductive types   Aaron Stump
• [Agda] defining coinductive types   Thierry Coquand
• [Agda] x ∈ (append y xs) → ..   Andreas Abel
• [Agda] Writing a paper in Literate Agda   Andreas Abel
• [Agda] defining coinductive types   Aaron Stump
• [Agda] defining coinductive types   Pierre-Evariste Dagand
• Non-strictly-positive types [Re: [Agda] defining coinductive types]   Andreas Abel
• [Agda] Writing a paper in Literate Agda   Ulf Norell
• Re: [Agda] x ∈ (append y xs) → ..   Ulf Norell
• [Agda] x ∈ (append y xs) → ..   Sergei Meshveliani
• [Agda] bug in definitions using "_"?   Martin Escardo
• [Agda] bug in definitions using "_"?   Ulf Norell
• [Agda] bug in definitions using "_"?   Martin Escardo
• [Agda] Showing Reflection.Name   Nils Anders Danielsson
• [Agda] finite map   Nils Anders Danielsson
• [Agda] finite map   Sergei Meshveliani
• [Agda] bug in definitions using "_"?   Jesper Cockx
• [Agda] TYPES Meeting 2014 in Paris, 12 - 15 May: first call for contributions   Matthieu Sozeau
• [Agda] bug in definitions using "_"?   Martin Escardo
• [Agda] " | condition " in report   Sergei Meshveliani
• [Agda] Postdoctoral Researcher at DemTech/IT University of Copenhagen   Carsten Schürmann
• [Agda] Call for Papers: ITP 2014   Gerwin Klein
• [Agda] \^r   Sergei Meshveliani
• [Agda] \^r   Twan van Laarhoven
• [Agda] UTP-2014 Unifying Theories of Programming - call for papers   David Naumann
• [Agda] " | condition " in report   Andreas Abel
• [Agda] Fake Conferences CSCI and WORLDCOMP of Hamid Arabnia   rickardbrown at hushmail.com
• [Agda] VMCAI 2014 call for participation   Kenneth McMillan
• [Agda] eta-equality for records and metavar resolution   Christian Sattler
• [Agda] eta-equality for records and metavar resolution   Andreas Abel
• [Agda] eta-equality for records and metavar resolution   Christian Sattler
• [Agda] " | condition " in report   Sergei Meshveliani
• [Agda] lists as sets   Sergei Meshveliani
• [Agda] eta-equality for records and metavar resolution   Andreas Abel
• [Agda] trivial lemma of `with'   Sergei Meshveliani
• [Agda] trivial lemma of `with'   Andreas Abel
• [Agda] eta-equality for records and metavar resolution   Christian Sattler
• [Agda] eta-equality for records and metavar resolution   Christian Sattler
• [Agda] eta-equality for records and metavar resolution   Christian Sattler

Last message date: Tue Dec 31 15:48:55 CEST 2013
Archived on: Tue Dec 31 15:45:36 CEST 2013

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