2014 Archives by date

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

Starting: Wed Jan 1 23:00:27 CEST 2014
Ending: Wed Dec 31 23:43:22 CEST 2014
Messages: 1121

• [Agda] eta-equality for records and metavar resolution   Andreas Abel
• [Agda] eta-equality for records and metavar resolution   Andreas Abel
• [Agda] trivial lemma of `with'   Sergei Meshveliani
• [Agda] withdraw AVL ≈ request?   Sergei Meshveliani
• [Agda] lists as sets   Nils Anders Danielsson
• github? [Re: [Agda] Agda development]   Jan Stolarek
• [Agda] trivial lemma of `with'   Andreas Abel
• [Agda] trivial lemma of `with'   Sergei Meshveliani
• [Agda] trivial lemma of `with'   Andreas Abel
• [Agda] trivial lemma of `with'   Sergei Meshveliani
• [Agda] 1st Call for Papers - TFPIE 2014   James Caldwell
• [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• [Agda] 1st CFP, Intersection Types and Related Systems 2014   Luca
• [Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Cody Roux
• [Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• [Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Maxime Dénès
• [Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Maxime Dénès
• [Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• [Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Cody Roux
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Vladimir Voevodsky
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Cody Roux
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Vladimir Voevodsky
• [Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Abhishek Anand
• [Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Maxime Dénès
• [Agda] [bug] make install does cabal update   Jan Stolarek
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• [Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   =?GB2312?B?RnKopmSopnJpYyBCbGFucXVp?=
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Martin Escardo
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Vladimir Voevodsky
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Vladimir Voevodsky
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Matthieu Sozeau
• [Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Conor McBride
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   =?GB2312?B?TWF4aW1lIESopm6oqHM=?=
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Conor McBride
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Prof. Robert Harper
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   =?GB2312?B?TWF4aW1lIESopm6oqHM=?=
• [Agda] [bug] make install does cabal update   Andreas Abel
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Dan Doel
• [Agda] ICFP 2014: Call for papers   David Van Horn
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Frédéric Blanqui
• [Agda] [bug] make install does cabal update   Ulf Norell
• [Agda] [bug] make install does cabal update   Jan Stolarek
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Conor McBride
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Matthieu Sozeau
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Jesper Cockx
• [Agda] CSL-LICS 2014 - Last Call for Papers   Andrzej Murawski
• [Agda] Re: Issue 1013 in agda: internal error, src/full/Agda/TypeChecking/Substitute.hs:322   Sergei Meshveliani
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Bruno Barras
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Jesper Cockx
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   =?GB2312?B?TWF4aW1lIESopm6oqHM=?=
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Cody Roux
• [Agda] Re: [Coq-Club] [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Andreas Abel
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Andreas Abel
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Aaron Stump
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Andreas Abel
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Aaron Stump
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Vladimir Voevodsky
• [Agda] y ≟ 0 for irrelevant y ≉ 0   Sergei Meshveliani
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Conor McBride
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Bruno Barras
• [Agda] Integer lemmata   Sergei Meshveliani
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Andrej Bauer
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Matthieu Sozeau
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Vladimir Voevodsky
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Andreas Abel
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Matthieu Sozeau
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Vladimir Voevodsky
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Matthieu Sozeau
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Jesper Cockx
• [Agda] Integer lemmata   Arseniy Alekseyev
• [Agda] Not understanding some goal solving stuff   Chris Moline
• [Agda] Re: Not understanding some goal solving stuff   Chris Moline
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Conor McBride
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Frédéric Blanqui
• github? [Re: [Agda] Agda development]   Ulf Norell
• github? [Re: [Agda] Agda development]   Mateusz Kowalczyk
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Frédéric Blanqui
• github? [Re: [Agda] Agda development]   Jan Stolarek
• github? [Re: [Agda] Agda development]   Mateusz Kowalczyk
• [Agda] Re: Not understanding some goal solving stuff   Andreas Abel
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Frédéric Blanqui
• github? [Re: [Agda] Agda development]   James Chapman
• [Agda] Joint 25th RTA & 12th TLCA: Final CALL FOR PAPERS   Luca Paolini
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• github? [Re: [Agda] Agda development]   Jan Stolarek
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Altenkirch Thorsten
• github? [Re: [Agda] Agda development]   Mateusz Kowalczyk
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Matthieu Sozeau
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Frédéric Blanqui
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Conor McBride
• github? [Re: [Agda] Agda development]   Jan Stolarek
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Bruno Barras
• github? [Re: [Agda] Agda development]   Andrés Sicard-Ramírez
• [Agda] Integer lemmata   Sergei Meshveliani
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Andrej Bauer
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Frédéric Blanqui
• [Agda] ANN: MiniAgda-0.2014.1.9 Toy language with dependent and sized types   Andreas Abel
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Andreas Abel
• [Agda] TeX capacity exceeded   Amr Sabry
• [Agda] ANN: MiniAgda-0.2014.1.9 Toy language with dependent and sized types   gallais
• [Agda] TeX capacity exceeded   Andreas Abel
• [Agda] TeX capacity exceeded   Andres Loeh
• [Agda] (s ◃ m ) * (s' ◃ n)   Sergei Meshveliani
• [Agda] (s ◃ m ) * (s' ◃ n)   Andreas Abel
• [Agda] (s ◃ m ) * (s' ◃ n)   Sergei Meshveliani
• [Agda] (s ◃ m ) * (s' ◃ n)   Sergei Meshveliani
• [Agda] Re: TeX capacity exceeded   Stevan Andjelkovic
• [Agda] assoc Sign._*_   Sergei Meshveliani
• [Agda] (s ◃ m ) * (s' ◃ n)   Andreas Abel
• [Agda] UTP-2014 Unifying Theories of Programming - call for papers   David Naumann
• [Agda] Re: Agda bug   Carlos Camarao
• [Agda] (s ◃ m ) * (s' ◃ n)   Sergei Meshveliani
• Inspect pattern needed? [Re: [Agda] Re: Agda bug]   Andreas Abel
• [Agda] Re: TeX capacity exceeded   Abhishek Anand
• [Agda] Simple monoid instance based on monoid instance of underlying type   Mateusz Kowalczyk
• [Agda] Re: TeX capacity exceeded   Stevan Andjelkovic
• [Agda] Simple monoid instance based on monoid instance of underlying type   James ‘Twey’ Kay
• [Agda] Simple monoid instance based on monoid instance of underlying type   Andreas Abel
• Inspect pattern needed? [Re: [Agda] Re: Agda bug]   Carlos Camarao
• [Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq   Andreas Abel
• github? [Re: [Agda] Agda development]   Jason Gross
• [Agda] Simple monoid instance based on monoid instance of underlying type   Mateusz Kowalczyk
• [Agda] Making ≡ proofs more manageable   Mateusz Kowalczyk
• [Agda] Making ≡ proofs more manageable   Andreas Abel
• [Agda] Making ≡ proofs more manageable   Mateusz Kowalczyk
• [Agda] Making ≡ proofs more manageable   Helmut Grohne
• [Agda] Making ≡ proofs more manageable   Andreas Abel
• [Agda] include agda in latex   Altenkirch Thorsten
• [Agda] Making ≡ proofs more manageable   Twan van Laarhoven
• [Agda] include agda in latex   Dominique Devriese
• [Agda] include agda in latex   Abhishek Anand
• [Agda] Re: include agda in latex   Stevan Andjelkovic
• [Agda] Making ≡ proofs more manageable   Mateusz Kowalczyk
• [Agda] default field values   Sergei Meshveliani
• [Agda] default field values   Sergei Meshveliani
• [Agda] Problem installing Agda OS X Mavericks   Wouter Swierstra
• [Agda] Problem installing Agda OS X Mavericks   Mateusz Kowalczyk
• [Agda] Problem installing Agda OS X Mavericks   Wouter Swierstra
• [Agda] The standard library has moved to github   Ulf Norell
• [Agda] Yet another way Agda --without-K is incompatible with univalence   Jesper Cockx
• [Agda] [PATCH] add a ∷-injective for Vec like there is one for List   Helmut Grohne
• [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Jesper Cockx
• [Agda] The standard library has moved to github   Nicolas Pouillard
• [Agda] [PATCH] add a ∷-injective for Vec like there is one for List   Andreas Abel
• Re: [Agda] [PATCH] add a ∷-injective for Vec like there is one for List   Altenkirch Thorsten
• [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Andreas Abel
• [Agda] [PATCH] add a ∷-injective for Vec like there is one for List   Twan van Laarhoven
• [Agda] [PATCH] add a ∷-injective for Vec like there is one for List   Andreas Abel
• Re: [Agda] [PATCH] add a ∷-injective for Vec like there is one for List   Altenkirch Thorsten
• [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Jesper Cockx
• [Agda] The standard library has moved to github   Andrés Sicard-Ramírez
• [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Andreas Abel
• [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Matthieu Sozeau
• Fwd: [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Matteo Acerbi
• [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Jesper Cockx
• [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Matteo Acerbi
• [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Jesper Cockx
• [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Matteo Acerbi
• [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Jesper Cockx
• [Agda] Yet another way Agda --without-K is incompatible with univalence   Nils Anders Danielsson
• [Agda] Re: The standard library has moved to github   Stevan Andjelkovic
• [Agda] Re: Yet another way Agda --without-K is incompatible with univalence   Matteo Acerbi
• [Agda] default field values   Wolfram Kahl
• [Agda] --no-pattern-matching   Andreas Abel
• [Agda] --no-pattern-matching   Guillaume Brunerie
• [Agda] --no-pattern-matching   Conor McBride
• [Agda] --no-pattern-matching   Andreas Abel
• [Agda] --no-pattern-matching   Andreas Abel
• Core and elaboration [Re: [Agda] --no-pattern-matching]   Andreas Abel
• [Agda] Re: The standard library has moved to github   Jason Gross
• [Agda] --no-pattern-matching   Matteo Acerbi
• [Agda] default field values   Sergei Meshveliani
• [Agda] default field values   Andreas Abel
• [Agda] Fwd: Hashtables: 'Basic' hashtables performance quirks on Win64   Andreas Abel
• [Agda] Re: Fwd: Hashtables: 'Basic' hashtables performance quirks on Win64   Andreas Abel
• Re: [Agda] [PATCH] add a ∷-injective for Vec like there is one for List   Vladimir Voevodsky
• Re: [Agda] [PATCH] add a ∷-injective for Vec like there is one for List   Jason Gross
• [Agda] Weird behaviour inside of ‘let’   Mateusz Kowalczyk
• Re: [Agda] Weird behaviour inside of ‘let’   Ulf Norell
• Re: [Agda] Weird behaviour inside of ‘let’   Ulf Norell
• [Agda] Weird behaviour inside of ‘let’   Mateusz Kowalczyk
• Re: [Agda] Weird behaviour inside of ‘let’   Ulf Norell
• [Agda] Re: The standard library has moved to github   Stevan Andjelkovic
• [Agda] question on irrelevant argument   Sergei Meshveliani
• [Agda] Re: The standard library has moved to github   Mateusz Kowalczyk
• [Agda] question on irrelevant argument   Ulf Norell
• [Agda] Re: The standard library has moved to github   Stevan Andjelkovic
• [Agda] Re: The standard library has moved to github   Jason Gross
• [Agda] Re: The standard library has moved to github   Stevan Andjelkovic
• [Agda] question on irrelevant argument   Sergei Meshveliani
• [Agda] Re: The standard library has moved to github   Jason Gross
• [Agda] question on irrelevant argument   Andreas Abel
• [Agda] Weird behaviour inside of ‘let’   Andreas Abel
• [Agda] Re: The standard library has moved to github   Stevan Andjelkovic
• [Agda] question on irrelevant argument   Sergei Meshveliani
• [Agda] question on irrelevant argument   Andreas Abel
• [Agda] Postdoctoral Researcher at DemTech/IT University of Copenhagen   Carsten Schürmann
• [Agda] Postdoctoral Researcher at DemTech/IT University of Copenhagen   Carsten Schürmann
• [Agda] GandALF 2014: Preliminary call for papers   murano at na.infn.it
• [Agda] Re: The standard library has moved to github   Ulf Norell
• [Agda] github on Standard library   Sergei Meshveliani
• [Agda] github on Standard library   Mateusz Kowalczyk
• [Agda] github on Standard library   Andrés Sicard-Ramírez
• [Agda] slow file with many constructors   Aaron Stump
• [Agda] slow file with many constructors   Liam O'Connor
• [Agda] Joint 25th RTA & 12th TLCA: Last reminder   Luca
• [Agda] f (p1 , p2)   Sergei Meshveliani
• [Agda] f (p1 , p2)   Andreas Abel
• [Agda] f (p1 , p2)   Sergei Meshveliani
• [Agda] slow file with many constructors   Nils Anders Danielsson
• [Agda] slow file with many constructors   Andreas Abel
• [Agda] slow file with many constructors   Aaron Stump
• [Agda] slow file with many constructors   Gabriel Scherer
• [Agda] slow file with many constructors   Andreas Abel
• [Agda] slow file with many constructors   Aaron Stump
• [Agda] Midlands Graduate School 2014, register now   Altenkirch Thorsten
• [Agda] Haskell Platform and Agda on OS X Mavericks/xcode 5   James Chapman
• [Agda] Haskell Platform and Agda on OS X Mavericks/xcode 5   Andrew Pitts
• [Agda] Haskell Platform and Agda on OS X Mavericks/xcode 5   Ulf Norell
• [Agda] Haskell Platform and Agda on OS X Mavericks/xcode 5   Harley Eades
• [Agda] Haskell Platform and Agda on OS X Mavericks/xcode 5   James Chapman
• [Agda] Unicode   Harley Eades
• [Agda] TFP 2014 - 2nd call for papers   Peter Achten
• [Agda] Joint 25th RTA & 12th TLCA: Deadline extension   Luca
• [Agda] Unicode   Nils Anders Danielsson
• [Agda] Unicode   Harley D. Eades III
• [Agda] dependent inverse transitivity   Alexander Altman
• [Agda] updating record field   Sergei Meshveliani
• [Agda] updating record field   Ulf Norell
• [Agda] C-c-C-n for NatShow.show n   Sergei Meshveliani
• [Agda] C-c-C-n for NatShow.show n   Andrés Sicard-Ramírez
• [Agda] C-c-C-n for NatShow.show n   Sergei Meshveliani
• [Agda] unnatural check cost   Sergei Meshveliani
• [Agda] wiki spam   Patrik Jansson
• [Agda] wiki spam   Altenkirch Thorsten
• [Agda] wiki spam   Andreas Abel
• [Agda] MAP 2014 - First announcement - Call for contributions   Cyril Cohen
• [Agda] RFC: R.B.HeterogeneousEquality + i-cong   Helmut Grohne
• [Agda] type check explosion   Sergei Meshveliani
• [Agda] RFC: R.B.HeterogeneousEquality + i-cong   Ulf Norell
• [Agda] RFC: R.B.HeterogeneousEquality + i-cong   Helmut Grohne
• [Agda] RFC: R.B.HeterogeneousEquality + i-cong   Ulf Norell
• [Agda] Int/(m) test   Sergei Meshveliani
• [Agda] 2nd Call for Papers - TFPIE 2014   Peter Achten
• [Agda] Re: Issue 1041 in agda: `Maybe' causes a great type-check cost   Sergei Meshveliani
• [Agda] isYes   Sergei Meshveliani
• [Agda] Level not an inductive type   F.Lockwood Morris
• [Agda] AI4FM 2014: Call for Short Contributions   Iain Whiteside
• [Agda] Level not an inductive type   Andrea Vezzosi
• [Agda] Unicode   Nils Anders Danielsson
• [Agda] RFC: R.B.HeterogeneousEquality + i-cong   Helmut Grohne
• [Agda] panic error message on Windows   Aaron Stump
• [Agda] Re: Issue 1050 in agda: how to reduce type check cost   Sergei Meshveliani
• [Agda] isYes   Andreas Abel
• [Agda] Oregon Programming Languages Summer School, 2014   Amal Ahmed
• [Agda] Trouble with the 'with' clause   Balaji Rao
• [Agda] Trouble with the 'with' clause   Liam O'Connor
• [Agda] merging identical proofs?   Kenichi Asai
• [Agda] isYes   Nils Anders Danielsson
• [Agda] merging identical proofs?   Twan van Laarhoven
• [Agda] Reflection on the Agda wiki   Andreas Abel
• [Agda] Re: Reflection on the Agda wiki   Andrés Sicard-Ramírez
• [Agda] Re: merging identical proofs?   Kenichi Asai
• [Agda] ATVA 2014: First Call for Papers   Franck Cassez
• [Agda] Re: merging identical proofs?   Andreas Abel
• [Agda] 2nd Call for Papers: Conf. Intelligent Computer Mathematics (CICM 2014)   Serge Autexier
• [Agda] (¬_ ∘ P) Respects   Sergei Meshveliani
• [Agda] TYPES 2014 in Paris, May 12 - 15: last call for contributions   Matthieu Sozeau
• [Agda] Re: panic error message on Windows   Aaron Stump
• [Agda] Re: panic error message on Windows   Andrea Vezzosi
• [Agda] Re: panic error message on Windows   Aaron Stump
• [Agda] Re: panic error message on Windows   Andrea Vezzosi
• [Agda] First Call for Papers: 8th Verification Workshop (VERIFY 2014), Focus Theme: Verification Beyond IT Systems   Serge Autexier
• [Agda] proof by patterns   Sergei Meshveliani
• [Agda] LFMTP 2014: Call for Papers   Amy Felty
• [Agda] proof by patterns   Andreas Abel
• [Agda] proof by patterns   Sergei Meshveliani
• [Agda] Call for Participation RAMiCS 2014   Peter Höfner
• [Agda] *Deadline extended* Final call for contributions AI4FM 2014   Iain Whiteside
• [Agda] APLAS 2014: Call for papers   James Chapman
• [Agda] LOPSTR 2014 - First Call for Papers   Maurizio Proietti
• [Agda] Sized types and Inspect idiom problem   Ernesto Copello
• [Agda] Sized types and Inspect idiom problem   Andrea Vezzosi
• [Agda] ANNOUNCE: Idris developers' meeting in Gothenburg, April 29-May 2, 2014   David Christiansen
• [Agda] Possible extension to pattern matching?   Andrea Vezzosi
• [Agda] Possible extension to pattern matching?   Adam Gundry
• [Agda] CICM 2014: Extended Deadline March 14th, 2014   Serge Autexier
• [Agda] Possible extension to pattern matching?   Andreas Abel
• [Agda] SBLP 2014 - Call for Papers   Rodrigo Ribeiro
• [Agda] Re: [Coq-Club] Propositional extensionality: the return of the revenge   Andreas Abel
• [Agda] Re: [Coq-Club] Propositional extensionality: the return of the revenge   Maxime Dénès
• [Agda] Re: [Coq-Club] Propositional extensionality: the return of the revenge   Altenkirch Thorsten
• [Agda] Re: [Coq-Club] Propositional extensionality: the return of the revenge   Andreas Abel
• [Agda] First CFP: Workshop on Generic Programming (WGP) 2014   José Pedro Magalhães
• [Agda] Agda fails to build on GHC 7.8   Jan Stolarek
• [Agda] Agda fails to build on GHC 7.8   Ulf Norell
• [Agda] Second Call for Papers for SD14, July 12-13, 2014, Vienna   Lutz Strassburger
• [Agda] Autophagia   Martin Escardo
• [Agda] A correctness proof for pattern matching without K   Jesper Cockx
• [Agda] A correctness proof for pattern matching without K   Andrea Vezzosi
• [Agda] Question regarding a simple "dependently typed IF-THEN-ELSE"   Konstantin Tretjakov
• [Agda] A correctness proof for pattern matching without K   Martin Escardo
• [Agda] A correctness proof for pattern matching without K   Jesper Cockx
• [Agda] Question regarding a simple "dependently typed IF-THEN-ELSE"   Andreas Abel
• [Agda] Question regarding a simple "dependently typed IF-THEN-ELSE"   Konstantin Tretjakov
• [Agda] Data.Rational   Amr Sabry
• [Agda] Question regarding a simple "dependently typed IF-THEN-ELSE"   Ulf Norell
• [Agda] Data.Rational   Andreas Abel
• [Agda] [TFP2014] Final Call For Papers   Peter Achten
• [Agda] Data.Rational   Li Nuo
• [Agda] Data.Rational   Andreas Abel
• [Agda] Data.Rational   Sergei Meshveliani
• [Agda] Data.Rational   Noam Zeilberger
• [Agda] Data.Rational   Li Nuo
• [Agda] Data.Rational   Li Nuo
• [Agda] Data.Rational   Andreas Abel
• [Agda] Data.Rational   Sergei Meshveliani
• [Agda] Data.Rational   Sergei Meshveliani
• [Agda] Data.Rational   Noam Zeilberger
• [Agda] Data.Rational   Jacques Carette
• [Agda] Data.Rational   Sergei Meshveliani
• [Agda] Data.Rational   Sergei Meshveliani
• [Agda] Data.Rational   Sergei Meshveliani
• [Agda] Midlands Graduate School 2014, register now   Altenkirch Thorsten
• [Agda] long type checking times in the development version   Martin Escardo
• [Agda] Haskell 2014: Call for papers   Wouter Swierstra
• [Agda] Data.Rational   Sergei Meshveliani
• Termination checker to blame for bad performance [Re: [Agda] long type checking times in the development version]   Andreas Abel
• [Agda] Dependently Typed Programming 2014 Call for Papers   Edwin Brady
• [Agda] using irrelevant field   Sergei Meshveliani
• [Agda] using irrelevant field   Andreas Abel
• [Agda] using irrelevant field   Sergei Meshveliani
• [Agda] using irrelevant field   Andreas Abel
• [Agda] Error when compiling Agda from Darcs repository by GHC 7.2   Dirk Ullrich
• [Agda] Error when compiling Agda from Darcs repository by GHC 7.2   Mateusz Kowalczyk
• [Agda] Error when compiling Agda from Darcs repository by GHC 7.2   Dirk Ullrich
• [Agda] Error when compiling Agda from Darcs repository by GHC 7.2   Andreas Abel
• [Agda] Error when compiling Agda from Darcs repository by GHC 7.2   Dirk Ullrich
• [Agda] Error when compiling Agda from Darcs repository by GHC 7.2   Ulf Norell
• [Agda] Error when compiling Agda from Darcs repository by GHC 7.2   Andreas Abel
• [Agda] ghc link options in MAlonzo?   Conor McBride
• [Agda] ghc link options in MAlonzo?   Mateusz Kowalczyk
• [Agda] ghc link options in MAlonzo?   Conor McBride
• [Agda] ghc link options in MAlonzo?   Matteo Acerbi
• [Agda] MAP 2014 Second announcement/Deadline extension   Cyril Cohen
• [Agda] Data.Rational   Amr Sabry
• [Agda] Data.Rational   Mateusz Kowalczyk
• [Agda] Data.Rational   Mateusz Kowalczyk
• [Agda] Data.Rational   Amr Sabry
• [Agda] Data.Rational   Mateusz Kowalczyk
• [Agda] Data.Rational   Andreas Abel
• [Agda] Side Effects in Agda   Joe M
• [Agda] Side Effects in Agda   Joe M
• [Agda] Side Effects in Agda   Andreas Abel
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Mateusz Kowalczyk
• [Agda] Agda meeting 22-28 May in Paris, call for participation   Andreas Abel
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Andreas Abel
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Mateusz Kowalczyk
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Tillmann Rendel
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Andreas Abel
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Mateusz Kowalczyk
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Mateusz Kowalczyk
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Bas Spitters
• [Agda] ATVA 2014: 2nd Call for Papers -- Sydney November 3-7   Franck Cassez
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Ulf Norell
• [Agda] Side Effects in Agda   Ulf Norell
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Nicolas Pouillard
• [Agda] AI4FM 2014: Call for Participation   Iain Whiteside
• [Agda] Side Effects in Agda   Joe M
• [Agda] Non-termination change in Agda 2.3.3   Mateusz Kowalczyk
• [Agda] Non-termination change in Agda 2.3.3   Ulf Norell
• [Agda] Non-termination change in Agda 2.3.3   Nicolas Pouillard
• [Agda] Non-termination change in Agda 2.3.3   Ulf Norell
• [Agda] Types Meeting 2014 in Paris, 12 - 15 May: call for participation   Hugo Herbelin
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Alan Jeffrey
• [Agda] MAlonzo performance   Sergei Meshveliani
• [Agda] MAlonzo performance   Mateusz Kowalczyk
• [Agda] MAlonzo performance   Aaron Stump
• [Agda] MAlonzo performance   Aaron Stump
• [Agda] MAlonzo performance   Alan Jeffrey
• [Agda] MAlonzo performance   Sergei Meshveliani
• [Agda] Building Agda on GHC 7.9   Mateusz Kowalczyk
• [Agda] Building Agda on GHC 7.9   Ulf Norell
• [Agda] Building Agda on GHC 7.9   kyra
• [Agda] Building Agda on GHC 7.9   Mateusz Kowalczyk
• [Agda] Third and Last Call for Papers for SD14, July 12-13, 2014, Vienna   Lutz Strassburger
• [Agda] One PhD position for EU students available at the University of Dundee, Scotland.   Marco Gaboardi
• [Agda] Building Agda on GHC 7.9   Andreas Abel
• [Agda] Functional Reactive Types   Alan Jeffrey
• [Agda] [TFP2014] First Call for Participation   Peter Achten
• [Agda] [TFPIE2014] final call for papers   Peter Achten
• [Agda] Functional Reactive Types   Andreas Abel
• [Agda] A correctness proof for pattern matching without K   Martin Escardo
• [Agda] Second CFP: Workshop on Generic Programming (WGP) 2014   José Pedro Magalhães
• [Agda] A correctness proof for pattern matching without K   Jesper Cockx
• [Agda] A correctness proof for pattern matching without K   Martin Escardo
• [Agda] A correctness proof for pattern matching without K   Jesper Cockx
• [Agda] A correctness proof for pattern matching without K   Martin Escardo
• [Agda] Classical Logic and Computation 2014 in Wien - extended deadline   Berardi Stefano
• [Agda] Autophagia   Nils Anders Danielsson
• [Agda] Generic programming and pointfree stuff.   flicky frans
• [Agda] Generic programming and pointfree stuff.   Andreas Abel
• [Agda] Generic programming and pointfree stuff.   flicky frans
• [Agda] Monads with polymorhic bind.   flicky frans
• [Agda] Generic programming and pointfree stuff.   Ulf Norell
• [Agda] Generic programming and pointfree stuff.   Andreas Abel
• [Agda] Generic programming and pointfree stuff.   flicky frans
• [Agda] Generic programming and pointfree stuff.   Nils Anders Danielsson
• [Agda] Generic programming and pointfree stuff.   Nils Anders Danielsson
• [Agda] Generic programming and pointfree stuff.   flicky frans
• [Agda] 2nd CfP, VERIFY 2014, 8th Verification Workshop, *Abstract Deadline April 17th, 2014*, Focus Theme: Verification Beyond IT Systems   Serge Autexier
• [Agda] Oregon PL Summer School: call for participation   Amal Ahmed
• [Agda] Software Engineering vacancy at Radboud University Nijmegen   Marko van Eekelen
• [Agda] LFMTP 2014: 2nd Call for Papers   Amy Felty
• [Agda] Generic programming and pointfree stuff.   Nils Anders Danielsson
• [Agda] Agda on GitHub Atom   Balaji Rao R
• [Agda] PhD Position in dependent types, testing & hardware design   Wouter Swierstra
• [Agda] Agda on GitHub Atom   Helmut Grohne
• [Agda] Summer School on Advances in Programming Langauges   Belikov, Evgenij
• [Agda] Agda on GitHub Atom   Balaji Rao R
• [Agda] Oregon PL Summer School: register by May 2nd   Amal Ahmed
• [Agda] Haskell Symposium: Second call for papers   Wouter Swierstra
• [Agda] ATVA 2014: Last Call for Papers -- Sydney November 3-7   Franck Cassez
• [Agda] ATVA 2014: Last Call for Papers -- Sydney November 3-7   Franck Cassez
• [Agda] LOLA 2014 - Call for Talk Proposals   Andrzej Murawski
• [Agda] Types Meeting 2014 in Paris, 12 - 15 May: 2nd call for participation   Hugo Herbelin
• [Agda] LOPSTR 2014: Second Call for Papers   Maurizio Proietti
• [Agda] Generic programming and pointfree stuff.   flicky frans
• [Agda] CfP: 8th Verification Workshop (VERIFY 2014), Focus Theme: Verification Beyond IT Systems, extended deadline *May 5th, 2014*   Serge Autexier
• [Agda] 2nd CFP: Dependently Typed Programming 2014   Edwin Brady
• [Agda] Spanish keyboard + Agda input-mode   Michael Shulman
• [Agda] A different implementation of --without-K   Andreas Abel
• [Agda] A different implementation of --without-K   Jesper Cockx
• [Agda] Spanish keyboard + Agda input-mode   Nils Anders Danielsson
• [Agda] A different implementation of --without-K   Andreas Abel
• [Agda] Agda on GitHub Atom   Nils Anders Danielsson
• [Agda] Strict application   Andrés Sicard-Ramírez
• [Agda] Agda on GitHub Atom   Balaji Rao R
• [Agda] Strict application   Dmytro Starosud
• [Agda] Strict application   Dmytro Starosud
• [Agda] Strict application   Andrés Sicard-Ramírez
• [Agda] Strict application   Wolfram Kahl
• [Agda] Strict application   Andrés Sicard-Ramírez
• [Agda] Strict application   Andreas Abel
• [Agda] A different implementation of --without-K   Jesper Cockx
• [Agda] A different implementation of --without-K   Andreas Abel
• [Agda] Call for talk proposals: HOPE'14 (Workshop on Higher-Order Programming with Effects, affiliated with ICFP'14)   Neelakantan Krishnaswami
• [Agda] GandALF 2014: Call for papers   murano
• [Agda] Types Meeting 2014 in Paris, 12 - 15 May: Last call for participation   Hugo Herbelin
• [Agda] Final CFP: Workshop on Generic Programming (WGP) 2014   José Pedro Magalhães
• [Agda] dependency graph   Martin Escardo
• [Agda] dependency graph   Nils Anders Danielsson
• [Agda] dependency graph   Martin Escardo
• [Agda] dependency graph   Tillmann Rendel
• [Agda] dependency graph   Martin Escardo
• [Agda] dependency graph   Tillmann Rendel
• [Agda] WADT 2014 - 1st Call for Papers   2014 wadt
• [Agda] MIND, MECHANISM AND MATHEMATICS at Columbia University, New York City, May 12-14, 2014 - registration open   S B Cooper
• [Agda] dependency graph   Nils Anders Danielsson
• [Agda] agda --latex inline code   Altenkirch Thorsten
• [Agda] [TFPIE2014] final call for participation   Peter Achten
• [Agda] agda --latex inline code   Stevan Andjelkovic
• [Agda] A proof of omniscience in Agda   Martin Escardo
• [Agda] agda --latex inline code   Altenkirch Thorsten
• [Agda] Deadline extended: Workshop on Generic Programming (WGP) 2014   José Pedro Magalhães
• [Agda] Domain Theory Libraries for Agda?   Clarissa Littler
• [Agda] Domain Theory Libraries for Agda?   Aaron Stump
• [Agda] Domain Theory Libraries for Agda?   Bas Spitters
• [Agda] Domain Theory Libraries for Agda?   Bas Spitters
• [Agda] First Call for Papers: 26. OpenMath Workshop (at CICM 2014; July 7. July 2014)   Michael Kohlhase
• [Agda] Known inconsistency not fixed in release for one year   Paolo G. Giarrusso
• [Agda] Re: Known inconsistency not fixed in release for one year   Paolo G. Giarrusso
• [Agda] GandALF 2014: Extended deadlines   aniello murano
• [Agda] agda --latex inline code   Stevan Andjelkovic
• [Agda] agda --latex inline code   Altenkirch Thorsten
• [Agda] Another library question: categories   Clarissa Littler
• [Agda] Another library question: categories   Harley D. Eades III
• [Agda] First call for papers IFL 2014   publicityifl at gmail.com
• [Agda] beamer \setbeamercolor{math text} destroys agda --latex colors for some characters   Andreas Abel
• [Agda] beamer \setbeamercolor{math text} destroys agda --latex colors for some characters   Stevan Andjelkovic
• [Agda] ICFP 2014 Student Research Competition: Call for Submissions   David Van Horn
• [Agda] Research position "Coalgebraic Logic Programming for Type Inference"   Ekaterina Komendantskaya
• [Agda] agda --latex inline code   Nils Anders Danielsson
• [Agda] agda --latex inline code   Nils Anders Danielsson
• [Agda] Known inconsistency not fixed in release for one year   Nils Anders Danielsson
• [Agda] One PhD position is available at the University of Dundee, Scotland   Ekaterina Komendantskaya
• [Agda] Fwd: [Haskell] APLAS 2014: Last CFP   James Chapman
• [Agda] Higher inductive-recursive definitions?   Altenkirch Thorsten
• [Agda] Higher inductive-recursive definitions?   Guillaume Brunerie
• [HoTT] Re: [Agda] Higher inductive-recursive definitions?   Altenkirch Thorsten
• [HoTT] Re: [Agda] Higher inductive-recursive definitions?   Jason Gross
• [HoTT] Re: [Agda] Higher inductive-recursive definitions?   Jason Gross
• [HoTT] Re: [Agda] Higher inductive-recursive definitions?   Peter LeFanu Lumsdaine
• [HoTT] Re: [Agda] Higher inductive-recursive definitions?   Altenkirch Thorsten
• [Agda] Fwd: [Haskell] APLAS 2014: Extended deadline   James Chapman
• [Agda] Second Workshop on Haskell And Rewriting Techniques (HART 2014, co-located with ICFP 2014)   Janis Voigtlaender
• [Agda] Universes in Coq   Vladimir Voevodsky
• [Agda] small oddity of DistributesOver in the standard library 0.7   Kenichi Asai
• [Agda] Student Volunteer Programme   David Van Horn
• [Agda] LFMTP 2014: Call for Participation   Amy Felty
• [Agda] ITP'14: early registration deadline approaching   Gerwin Klein
• [Agda] Release: Agda 2.4.0   Ulf Norell
• [Agda] Release: Agda 2.4.0   Dominique Devriese
• [Agda] Release: Agda 2.4.0   Ulf Norell
• [Agda] Termination checker change?   Pierre Hyvernat
• [Agda] Constructors are injective -- standard proof?   Jacques Carette
• [Agda] Termination checker change?   Andreas Abel
• [Agda] Constructors are injective -- standard proof?   Helmut Grohne
• [Agda] WADT 2014 - 2nd Call for Papers   2014 wadt
• [Agda] Termination checker change?   Pierre Hyvernat
• [Agda] Termination checker change?   Andreas Abel
• [Agda] Final call for talk proposals: HOPE'14 (Workshop on Higher-Order Programming with Effects, affiliated with ICFP'14)   Neelakantan Krishnaswami
• [Agda] Constructors are injective -- standard proof?   Andreas Abel
• [Agda] Postdoctoral Research Position: Type Inference in Functional Programming   Ekaterina Komendantskaya
• [Agda] small oddity of DistributesOver in the standard library 0.7   Nils Anders Danielsson
• [Agda] Constructors are injective -- standard proof?   Nils Anders Danielsson
• [Agda] Equations should hold definitionally whenever possible   Jesper Cockx
• [Agda] Standard library for Agda-2.4.0   Ulf Norell
• [Agda] Agda moving to GitHub   Ulf Norell
• [Agda] Agda moving to GitHub   Mateusz Kowalczyk
• [Agda] Agda moving to GitHub   Andreas Abel
• [Agda] Agda moving to GitHub   Ulf Norell
• [Agda] Agda moving to GitHub   Jason Dagit
• [Agda] Agda moving to GitHub   Ulf Norell
• [Agda] Agda moving to GitHub   Tillmann Rendel
• [Agda] Vienna Summer of Logic: Call for participation   Sophie Tison
• [Agda] Standard library for Agda-2.4.0   Sergei Meshveliani
• [Agda] Agda moving to GitHub   Ulf Norell
• [Agda] Standard library for Agda-2.4.0   Andrés Sicard-Ramírez
• [Agda] Standard library for Agda-2.4.0   Wolfram Kahl
• [Agda] ANNOUNCE: Standard library version 0.8   Andrés Sicard-Ramírez
• [Agda] Agda's copatterns incompatible with initial algebras   Dmitriy Traytel
• [Agda] Agda's copatterns incompatible with initial algebras   Andrea Vezzosi
• [Agda] Agda's copatterns incompatible with initial algebras   Dmitriy Traytel
• [Agda] Agda's copatterns incompatible with initial algebras   Andrea Vezzosi
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Brent Yorgey
• [Agda] adding StrictTotalOrder for Integer   Sergei Meshveliani
• [Agda] Agda's copatterns incompatible with initial algebras   Andreas Abel
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Andrés Sicard-Ramírez
• [Agda] Wrong number of commits on GitHub   Andrés Sicard-Ramírez
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Peter Hancock
• [Agda] Refactoring typechecking monads   Favonia
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Brent Yorgey
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Brent Yorgey
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Andrés Sicard-Ramírez
• [Agda] Refactoring typechecking monads   Ulf Norell
• [Agda] Agda 2.4.0.1   Ulf Norell
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Andrés Sicard-Ramírez
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Jesper Cockx
• [Agda] universum levels   Sergei Meshveliani
• [Agda] Refactoring typechecking monads   Favonia
• [Agda] Refactoring typechecking monads   Ulf Norell
• [Agda] (no subject)   Tobias Wrigstad
• [Agda] (no subject)   Ernesto Copello
• [Agda] (no subject)   Andreas Abel
• [Agda] universum levels   Andreas Abel
• [Agda] (no subject)   Ernesto Copello
• [Agda] universum levels   Ulf Norell
• [Agda] universum levels   Sergei Meshveliani
• [Agda] universum levels   Sergei Meshveliani
• [Agda] ICFP Call for Participation   David Van Horn
• [Agda] universe levels   Martin Escardo
• [Agda] universum levels   Abhishek Anand
• Sizes should be irrelevant in constructors [Re: [Agda] (no subject)]   Andreas Abel
• [Agda] (no subject)   Andrea Vezzosi
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Dan Licata
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Jesper Cockx
• [Agda] SSTiC 2014: last-minute half-price registration   GRLMC
• [Agda] Records with parameters depending on fields?   Joachim Breitner
• [Agda] Records with parameters depending on fields?   Twan van Laarhoven
• [Agda] Game of Life   Christopher Jenkins
• [Agda] Kruskal's theorem   Sergei Meshveliani
• [Agda] Kruskal's theorem   Frédéric Blanqui
• [Agda] Kruskal's theorem   Sergei Meshveliani
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Frédéric Blanqui
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Dan Licata
• [Agda] pattern matching on records   Amr Sabry
• [Agda] pattern matching on records   Twan van Laarhoven
• [Agda] pattern matching on records   Amr Sabry
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Jesper Cockx
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Jesper Cockx
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Dmytro Starosud
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Dmytro Starosud
• [Agda] termination by contradiction   Altenkirch Thorsten
• [Agda] termination by contradiction   Dmytro Starosud
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Dan Licata
• [Agda] termination by contradiction   Peter Hancock
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Altenkirch Thorsten
• [Agda] termination by contradiction   Altenkirch Thorsten
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Maxime Dénès
• [Agda] termination by contradiction   Ulf Norell
• [Agda] termination by contradiction   Altenkirch Thorsten
• [Agda] termination by contradiction   Dmytro Starosud
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Ulf Norell
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Dmytro Starosud
• [Agda] termination by contradiction   Ulf Norell
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Twan van Laarhoven
• [Agda] termination by contradiction   Ulf Norell
• [Agda] termination by contradiction   Martin Escardo
• [Agda] termination by contradiction   gallais
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Ulf Norell
• [Agda] Ramsey theorem   Sergei Meshveliani
• [Agda] Ramsey theorem   Josef Svenningsson
• [Agda] Ramsey theorem   David Wahlstedt
• [Agda] Ramsey theorem   Sergei Meshveliani
• [Agda] termination by contradiction   Dan Licata
• [Agda] termination by contradiction   Ulf Norell
• [Agda] termination by contradiction   Andreas Abel
• [Agda] termination by contradiction   Andrés Sicard-Ramírez
• [Agda] termination by contradiction   Ulf Norell
• [Agda] Re: Issue 1225 in agda: cannot build Development Agda of July 5, 2014   Sergei Meshveliani
• [Agda] termination by contradiction   Nicolas Pouillard
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Ulf Norell
• [Agda] Re: Issue 1225 in agda: cannot build Development Agda of July 5, 2014   Andrés Sicard-Ramírez
• [Agda] termination by contradiction   Ulf Norell
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Sergei Meshveliani
• [Agda] termination by contradiction   Ulf Norell
• [Agda] Ramsey theorem   Danko Ilik
• [Agda] Ramsey theorem   Sergei Meshveliani
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Dan Licata
• [Agda] Recursive instance search   Guillaume Brunerie
• [Agda] Recursive instance search   Ulf Norell
• [Agda] PEPM 2015 call for papers   Andreas Abel
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Jesper Cockx
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Andreas Abel
• [Agda] Recursive instance search   Ulf Norell
• [Agda] Recursive instance search   Ulf Norell
• POSTUlATE_TERMINATION --- Was: Re: [Agda] termination by contradiction   Wolfram Kahl
• POSTUlATE_TERMINATION --- Was: Re: [Agda] termination by contradiction   Harley D. Eades III
• [Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?   Dan Licata
• POSTUlATE_TERMINATION --- Was: Re: [Agda] termination by contradiction   Andreas Abel
• POSTUlATE_TERMINATION --- Was: Re: [Agda] termination by contradiction   Andreas Abel
• [Agda] Without-K puzzle   Ulf Norell
• [Agda] Without-K puzzle   Jesper Cockx
• [Agda] Without-K puzzle   Ulf Norell
• [Agda] Interactive copattern splitting   Andreas Abel
• [Agda] Without-K puzzle   Ulf Norell
• [Agda] Interactive copattern splitting   Ulf Norell
• [Agda] Without-K puzzle   Vladimir Voevodsky
• [Agda] Without-K puzzle   Martin Escardo
• [Agda] Without-K puzzle   Martin Escardo
• [Agda] unification and HITs   Dan Licata
• POSTUlATE_TERMINATION --- Was: Re: [Agda] termination by contradiction   Wolfram Kahl
• POSTUlATE_TERMINATION --- Was: Re: [Agda] termination by contradiction   Dominique Devriese
• POSTUlATE_TERMINATION --- Was: Re: [Agda] termination by contradiction   Wolfram Kahl
• POSTUlATE_TERMINATION --- Was: Re: [Agda] termination by contradiction   Dominique Devriese
• [Agda] CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call)   Hugo Herbelin
• [Agda] Strange error when trying to install Agda 2.4.0.1 from cabal   Christopher Jenkins
• [Agda] Strange error when trying to install Agda 2.4.0.1 from cabal   Andrés Sicard-Ramírez
• [Agda] Strange error when trying to install Agda 2.4.0.1 from cabal   Christopher Jenkins
• [Agda] Data.Vec toList - fromList isomorphism   Dan Krejsa
• [Agda] Re: Data.Vec toList - fromList isomorphism   Dan Krejsa
• [Agda] Re: Data.Vec toList - fromList isomorphism   Ulf Norell
• [Agda] Re: Data.Vec toList - fromList isomorphism   Dan Krejsa
• [Agda] ICFP Programming Contest 2014   Nicolas Wu
• [Agda] HOPE 2014 Call for Participation (with Workshop Program)   Hongseok Yang
• [Agda] LOPSTR 2014: Call for Participation   Maurizio Proietti
• [Agda] Call for Papers PSC track at SAC 2015   Emiliano Tramontana
• [Agda] Maintenance status of Agda dependencies   Joachim Breitner
• [Agda] AIM XX   Jesper Cockx
• [Agda] Maintenance status of Agda dependencies   Andreas Abel
• [Agda] Maintenance status of Agda dependencies   Joachim Breitner
• [Agda] Re: Data.Vec toList - fromList isomorphism   AndrásKovács
• [Agda] Maintenance status of Agda dependencies   Andreas Abel
• [Agda] Agda 2.4.0.2 released   Andreas Abel
• [Agda] Theoretical limits of termination checking (reference request)   Kirill Elagin
• [Agda] Agda executables names   Andrés Sicard-Ramírez
• [Agda] Theoretical limits of termination checking (reference request)   Andreas Abel
• [Agda] Theoretical limits of termination checking (reference request)   Altenkirch Thorsten
• [Agda] Theoretical limits of termination checking (reference request)   Kirill Elagin
• [Agda] Theoretical limits of termination checking (reference request)   Andreas Abel
• [Agda] ICFP 2014 Final Call for Participation   David Van Horn
• [Agda] Haskell Symposium – Call for participation   Wouter Swierstra
• [Agda] Theoretical limits of termination checking (reference request)   Thomas Jaeger
• [Agda] with vs case example   Sergei Meshveliani
• [Agda] "data Null" for List   Sergei Meshveliani
• [Agda] about Null   Sergei Meshveliani
• [Agda] about Null   Sergei Meshveliani
• [Agda] hiding implementation   Sergei Meshveliani
• [Agda] hiding implementation   Mateusz Kowalczyk
• [Agda] hiding implementation   Dominique Devriese
• [Agda] all-P ?   Sergei Meshveliani
• [Agda] Second call for papers IFL 2014   planpublicity at gmail.com
• [Agda] all-P ?   Nils Anders Danielsson
• [Agda] Sized types problem   Roly Perera
• [Agda] Fully funded PhD position on Computational Logic/Functional Programming/Interactive Theorem Proving, University of Dundee, Scotland   Ekaterina Komendantskaya
• [Agda] Sized types problem   Andrea Vezzosi
• [Agda] 2nd CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call)   Hugo Herbelin
• [Agda] irrelevant arg example   Sergei Meshveliani
• [Agda] irrelevant arg example   Ulf Norell
• [Agda] Agda-mode and imported names   Pepijn Kokke
• [Agda] Agda-mode and imported names   Andrea Vezzosi
• [Agda] Agda-mode and imported names   Pepijn Kokke
• [Agda] irrelevant arg example   Sergei Meshveliani
• [Agda] LATA 2015: 2nd call for papers   GRLMC - URV
• [Agda] explicit irrelevance   Sergei Meshveliani
• [Agda] --jobs?   Mateusz Kowalczyk
• [Agda] Agda environment: Hackage, Hoogle, Haddock, Cabal?   Mateusz Kowalczyk
• [Agda] --jobs?   Ulf Norell
• [Agda] --jobs?   Andreas Abel
• [Agda] --jobs?   Mateusz Kowalczyk
• [Agda] --jobs?   Wolfram Kahl
• [Agda] Positivity of members of Set   Owen
• [Agda] Positivity of members of Set   Andreas Abel
• [Agda] Termination problem with --without-K   Jacques Carette
• [Agda] Termination problem with --without-K   Andreas Abel
• [Agda] Termination problem with --without-K   Andreas Abel
• [Agda] Agda 2.4.2   Ulf Norell
• [Agda] ANNOUNCE: Standard library version 0.8.1   Andrés Sicard-Ramírez
• [Agda] Final CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call, extended deadline)   Hugo Herbelin
• [Agda] foo ∘ fromFoo strangeness   Sergei Meshveliani
• Re: [Agda] foo ∘ fromFoo strangeness   Dmytro Starosud
• [Agda] foo ∘ fromFoo strangeness   Twan van Laarhoven
• [Agda] Third call for papers, IFL 2014   publicityifl at gmail.com
• [Agda] --jobs?   Thorsten Altenkirch
• [Agda] Theoretical limits of termination checking (reference request)   Frédéric Blanqui
• [Agda] Theoretical limits of termination checking (reference request)   Francisco Mota
• [Agda] Theoretical limits of termination checking (reference request)   Francisco Mota
• [Agda] Working with Agda inside nix-shell   Mateusz Kowalczyk
• [Agda] Working with Agda inside nix-shell   Andreas Abel
• [Agda] Working with Agda inside nix-shell   Mateusz Kowalczyk
• [Agda] AIM XX in Tallinn 16-22 October 2014   James Chapman
• [Agda] postdoc position(s) announcement   Vladimir Voevodsky
• [Agda] ATVA 2014: Call for Participation   Franck
• [Agda] Agda meeting (AIM XX) in Tallinn 16-22 October (one month tomorrow!)   James Chapman
• [Agda] Re: [Coq-Club] Questions about two theorems   Thorsten Altenkirch
• [Agda] Re: [Coq-Club] Questions about two theorems   Cedric Auger
• [Agda] AIM XX registration now open!   James Chapman
• [Agda] with -> case example   Sergei Meshveliani
• [Agda] strange " ,′ "   Sergei Meshveliani
• [Agda] strange " ,′ "   Andreas Abel
• [Agda] untabify: Warning to those that have forked Agda   Andreas Abel
• [Agda] Agda and GHC 7.8   Jan Stolarek
• [Agda] Agda and GHC 7.8   Andrés Sicard-Ramírez
• [Agda] Agda and GHC 7.8   Jan Stolarek
• [Agda] Agda and GHC 7.8   Andrés Sicard-Ramírez
• [Agda] Agda and GHC 7.8   Jan Stolarek
• [Agda] Agda and GHC 7.8   Andrés Sicard-Ramírez
• [Agda] Agda and GHC 7.8   Roly Perera
• [Agda] Agda and GHC 7.8   Jan Stolarek
• [Agda] font issue in emacs mode   Martin Escardo
• [Agda] Agda and GHC 7.8   Andreas Abel
• [Agda] Agda and GHC 7.8   Jan Stolarek
• [Agda] font issue in emacs mode   Paolo Capriotti
• [Agda] font issue in emacs mode   Andreas Abel
• [Agda] font issue in emacs mode   Andrés Sicard-Ramírez
• [Agda] font issue in emacs mode   Martin Escardo
• [Agda] font issue in emacs mode   Andreas Abel
• [Agda] Agda and GHC 7.8   Andreas Abel
• [Agda] Agda and GHC 7.8   Jan Stolarek
• [Agda] Agda and GHC 7.8   Andreas Abel
• [Agda] Size limit on generated code?   Roly Perera
• [Agda] Agda and GHC 7.8   Jan Stolarek
• [Agda] Size limit on generated code?   Andreas Abel
• [Agda] Agda and GHC 7.8   Twan van Laarhoven
• [Agda] Agda and GHC 7.8   Kyra
• [Agda] Agda and GHC 7.8   Andrés Sicard-Ramírez
• [Agda] Size limit on generated code?   flicky frans
• [Agda] Size limit on generated code?   Andreas Abel
• [Agda] Size limit on generated code?   flicky frans
• [Agda] Size limit on generated code?   Andreas Abel
• [Agda] Size limit on generated code?   Roly Perera
• [Agda] Status of Agda libraries   Mateusz Kowalczyk
• [Agda] Agda and GHC 7.8   Liam O'Connor
• [Agda] Agda and GHC 7.8   Liam O'Connor
• [Agda] Size limit on generated code?   Andreas Abel
• [Agda] Agda and GHC 7.8   Andrés Sicard-Ramírez
• [Agda] Agda and GHC 7.8   Andreas Abel
• [Agda] How much memory do I need to compile Agda 2.4.2?   Gyesik Lee
• [Agda] How much memory do I need to compile Agda 2.4.2?   Mateusz Kowalczyk
• [Agda] Agda and GHC 7.8   Jan Stolarek
• [Agda] Size limit on generated code?   Roly Perera
• [Agda] Normalization by evaluation, plain Agda types and impredicativity.   flicky frans
• [Agda] Re: Normalization by evaluation, plain Agda types and impredicativity.   Kenichi Asai
• [Agda] Re: Normalization by evaluation, plain Agda types and impredicativity.   flicky frans
• [Agda] Agda and GHC 7.8   Andrés Sicard-Ramírez
• [Agda] Agda and GHC 7.8   Jan Stolarek
• [Agda] Size limit on generated code?   Wolfram Kahl
• [Agda] Size limit on generated code?   Peter Hancock
• [Agda] AIM XX in Tallinn - 4 days left to register   James Chapman
• [Agda] Size limit on generated code?   Roly Perera
• [Agda] Size limit on generated code?   Roly Perera
• [Agda] How much memory do I need to compile Agda 2.4.2?   Andreas Abel
• [Agda] Re: Normalization by evaluation, plain Agda types and impredicativity.   Andreas Abel
• [Agda] Re: Normalization by evaluation, plain Agda types and impredicativity.   Andrea Vezzosi
• [Agda] Size limit on generated code?   Andreas Abel
• [Agda] Agda and GHC 7.8   Andrés Sicard-Ramírez
• [Agda] Re: Normalization by evaluation, plain Agda types and impredicativity.   flicky frans
• [Agda] Re: Normalization by evaluation, plain Agda types and impredicativity.   Andrea Vezzosi
• [Agda] Re: Normalization by evaluation, plain Agda types and impredicativity.   flicky frans
• [Agda] Tactics in Agda   Jesper Cockx
• [Agda] wiki empty?   Martin Escardo
• [Agda] wiki empty?   Andreas Abel
• [Agda] Tactics in Agda   gallais
• [Agda] Tactics in Agda   Wouter Swierstra
• [Agda] Size limit on generated code?   Andreas Abel
• [Agda] Size limit on generated code?   Andreas Abel
• [Agda] Size limit on generated code?   Nils Anders Danielsson
• [Agda] Size limit on generated code?   Edwin Brady
• [Agda] Embedded universe polymorphic programming.   flicky frans
• [Agda] Embedded universe polymorphic programming.   Frédéric Blanqui
• [Agda] Embedded universe polymorphic programming.   Vladimir Voevodsky
• [Agda] Embedded universe polymorphic programming.   Andreas Abel
• [Agda] Embedded universe polymorphic programming.   flicky frans
• [Agda] Restrictions on 'with' introductions?   Dan Krejsa
• [Agda] windows installation instructions   Thorsten Altenkirch
• [Agda] windows installation instructions   Mateusz Kowalczyk
• [Agda] Restrictions on 'with' introductions?   Andreas Abel
• [Agda] ICFP 2015 Call for Workshop and Co-located Event Proposals   David Van Horn
• [Agda] Mathematics of Program Construction (MPC 2015): first call for papers   José Pedro Magalhães
• [Agda] Restrictions on 'with' introductions?   Nils Anders Danielsson
• [Agda] Restrictions on 'with' introductions?   Andrea Vezzosi
• [Agda] Restrictions on 'with' introductions?   Andrea Vezzosi
• [Agda] map⊆   Sergei Meshveliani
• [Agda] map⊆   Nils Anders Danielsson
• [Agda] map⊆   Sergei Meshveliani
• [Agda] Restrictions on 'with' introductions?   Dan Krejsa
• [Agda] LICS 2015 - First Call for Papers   Andrzej Murawski
• [Agda] Theoretical limits of termination checking (reference request)   Kirill Elagin
• [Agda] Theoretical limits of termination checking (reference request)   Kirill Elagin
• [Agda] (Stronger) double negation of law of excluded middle   Dmytro Starosud
• [Agda] (Stronger) double negation of law of excluded middle   Daniel Peebles
• [Agda] (Stronger) double negation of law of excluded middle   Paolo Capriotti
• [Agda] (Stronger) double negation of law of excluded middle   Dmytro Starosud
• [Agda] (Stronger) double negation of law of excluded middle   Dmytro Starosud
• [Agda] (Stronger) double negation of law of excluded middle   Paolo Capriotti
• [Agda] (Stronger) double negation of law of excluded middle   Dmytro Starosud
• [Agda] Expanding literate Agda   Pepijn Kokke
• [Agda] (Stronger) double negation of law of excluded middle   Arseniy Alekseyev
• [Agda] (Stronger) double negation of law of excluded middle   Paolo Capriotti
• [Agda] (Stronger) double negation of law of excluded middle   Paolo Capriotti
• [Agda] (Stronger) double negation of law of excluded middle   Dmytro Starosud
• [Agda] Expanding literate Agda   Andrés Sicard-Ramírez
• [Agda] Expanding literate Agda   Ulf Norell
• [Agda] Expanding literate Agda   Andreas Abel
• [Agda] Expanding literate Agda   João Paulo Pizani Flor
• [Agda] Expanding literate Agda   Dominique Devriese
• [Agda] Expanding literate Agda   Pepijn Kokke
• [Agda] Expanding literate Agda   Pepijn Kokke
• [Agda] Expanding literate Agda   Andreas Abel
• [Agda] Expanding literate Agda   Sergey Kotikov
• [Agda] simple question   Andrew Harris
• [Agda] simple question   Mateusz Kowalczyk
• [Agda] simple question   Kyle Miller
• [Agda] simple question   Andreas Abel
• [Agda] (Stronger) double negation of law of excluded middle   Thorsten Altenkirch
• [Agda] simple question   silvio at cs.ioc.ee
• [Agda] simple question   Andrew Harris
• [Agda] simple question   Andreas Abel
• [Agda] (Stronger) double negation of law of excluded middle   Paolo Capriotti
• [Agda] (Stronger) double negation of law of excluded middle   Dmytro Starosud
• [Agda] (Stronger) double negation of law of excluded middle   Paolo Capriotti
• [Agda] (Stronger) double negation of law of excluded middle   Peter Hancock
• [Agda] (Stronger) double negation of law of excluded middle   Paolo Capriotti
• [Agda] (Stronger) double negation of law of excluded middle   Andrea Vezzosi
• [Agda] (Stronger) double negation of law of excluded middle   Kirill Elagin
• [Agda] (Stronger) double negation of law of excluded middle   Kirill Elagin
• [Agda] (Stronger) double negation of law of excluded middle   Peter Hancock
• [Agda] Internal error at src/full/Agda/TypeChecking/Substitute.hs:144   Helmut Grohne
• [Agda] Internal error at src/full/Agda/TypeChecking/Substitute.hs:144   Andrés Sicard-Ramírez
• [Agda] Internal error at src/full/Agda/TypeChecking/Substitute.hs:144   Helmut Grohne
• [Agda] TLCA: 1st CALL for PAPERS   Luca
• [Agda] TLCA: 1st CALL for PAPERS   Thorsten Altenkirch
• [Agda] map⊆   Nils Anders Danielsson
• [Agda] map⊆   Sergei Meshveliani
• [Agda] explicit irrelevance question   Sergei Meshveliani
• [Agda] explicit irrelevance question   Andreas Abel
• [Agda] explicit irrelevance question   Darius Jahandarie
• [Agda] explicit irrelevance question   Sergei Meshveliani
• [Agda] CFP: Relational and Algebraic Methods in Computer Science (RAMiCS 2015)   Michael Winter
• [Agda] Info on interacting with the Agda process   Mateusz Kowalczyk
• [Agda] Info on interacting with the Agda process   Andrés Sicard-Ramírez
• [Agda] Info on interacting with the Agda process   Andreas Abel
• [Agda] Info on interacting with the Agda process   Mateusz Kowalczyk
• [Agda] ICALP 2015 first call for papers   Andreas Abel
• [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...   Sergei Meshveliani
• Re: [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...   Paolo Capriotti
• Re: [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...   Abhishek Anand
• [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...   Sergei Meshveliani
• Re: [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...   Paolo Capriotti
• [Agda] Puzzled about how instance arguments work in the presence of metas   Jesper Cockx
• [Agda] Puzzled about how instance arguments work in the presence of metas   Guillaume Brunerie
• [Agda] Puzzled about how instance arguments work in the presence of metas   Jesper Cockx
• [Agda] `with' -> `case' example   Sergei Meshveliani
• [Agda] `with' -> `case' example   Andreas Abel
• [Agda] `with' -> `case' example   mechvel at scico.botik.ru
• [Agda] `with' -> `case' example   Sergei Meshveliani
• [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...   Nils Anders Danielsson
• [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...   Andreas Abel
• Re: [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...   flicky frans
• Re: [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...   flicky frans
• [Agda] join 2 `with'|   mechvel at scico.botik.ru
• [Agda] join 2 `with'|   Arseniy Alekseyev
• [Agda] join 2 `with'|   Andreas Abel
• [Agda] join 2 `with'|   Arseniy Alekseyev
• [Agda] join 2 `with'|   Christopher Jenkins
• [Agda] join 2 `with'|   Arseniy Alekseyev
• [Agda] join 2 `with'|   Christopher Jenkins
• [Agda] join 2 `with'|   Sergei Meshveliani
• [Agda] join 2 `with'|   Arseniy Alekseyev
• New issue 1342 [Re: [Agda] join 2 `with'|]   Andreas Abel
• [Agda] Severe performance regression on master   Andreas Abel
• [Agda] release schedule, coding suggestions, book   Aaron Stump
• [Agda] Severe performance regression on master   Joachim Breitner
• [Agda] join 2 `with'|   Christopher Jenkins
• [Agda] join 2 `with'|   Andreas Abel
• [Agda] difficult module instantiation   Sergei Meshveliani
• [Agda] ICFP 2015: Call for Papers   David Van Horn
• [Agda] Termination checking   Francesco Mazzoli
• [Agda] Termination checking   Andreas Abel
• [Agda] Termination checking   Andreas Abel
• [Agda] Termination checking   Andreas Abel
• [Agda] Termination checking   Francesco Mazzoli
• [Agda] question on parametric modules   Sergei Meshveliani
• [Agda] RDP 2015 Last Call for Workshops   Aleksy Schubert
• [Agda] Severe performance regression on master   Andreas Abel
• [Agda] release schedule, coding suggestions, book   Andreas Abel
• [Agda] First CFP CICM 2015   Serge Autexier
• [Agda] release schedule, coding suggestions, book   Aaron Stump
• [Agda] ANNOUNCE: Agda 2.4.2.1   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Standard library 0.9   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Standard library 0.9   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.1   Sergei Meshveliani
• [Agda] ANNOUNCE: Standard library 0.9   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.1   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Standard library 0.9   Wolfram Kahl
• [Agda] ANNOUNCE: Agda 2.4.2.1   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.1   Twan van Laarhoven
• [Agda] ANNOUNCE: Agda 2.4.2.1   Andreas Abel
• [Agda] ANNOUNCE: Agda 2.4.2.1   Andreas Abel
• [Agda] ANNOUNCE: Agda 2.4.2.1   silvio at cs.ioc.ee
• [Agda] ANNOUNCE: Agda 2.4.2.1   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.1   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.1   silvio at cs.ioc.ee
• [Agda] 2.4.2.1 installation issue   Aaron Stump
• [Agda] join 2 `with'|   Christopher Jenkins
• [Agda] 2.4.2.1 installation issue   Andrea Vezzosi
• [Agda] 2.4.2.1 installation issue   Aaron Stump
• [Agda] 2.4.2.1 installation issue   Andreas Abel
• [Agda] 2.4.2.1 installation issue   Aaron Stump
• [Agda] Final Call - 12th Annual Conference on Theory and Applications of Models of Computation (TAMC 2015), Singapore 18-20 May, 2015   CIE (S B Cooper)
• [Agda] strange PE.refl ambiguity   Sergei Meshveliani
• [Agda] join 2 `with'|   Gabriel Scherer
• [Agda] 2.4.2.1 installation issue   Aaron Stump
• [Agda] 2.4.2.1 installation issue   Andrés Sicard-Ramírez
• [Agda] join 2 `with'|   Christopher Jenkins
• [Agda] 2.4.2.1 installation issue   Aaron Stump
• [Agda] Possible bug when using "with" on a partially applied function   Christopher Jenkins
• [Agda] Re: Possible bug when using "with" on a partially applied function   Christopher Jenkins
• [Agda] Re: Possible bug when using "with" on a partially applied function   Andreas Abel
• [Agda] Re: Possible bug when using "with" on a partially applied function   Andrea Vezzosi
• [Agda] Re: Possible bug when using "with" on a partially applied function   Andreas Abel
• [Agda] Telescope syntax   Guillaume Brunerie
• [Agda] ANNOUNCE: Agda 2.4.2.2   Andrés Sicard-Ramírez
• [Agda] Telescope syntax   Jesper Cockx
• [Agda] Telescope syntax   Jon Sterling
• [Agda] Re: ANNOUNCE: Agda 2.4.2.2   Andrés Sicard-Ramírez
• [Agda] Telescope syntax   Liam O'Connor
• [Agda] Telescope syntax   Jason Gross
• [Agda] Telescope syntax   Jon Sterling
• [Agda] Telescope syntax   Jon Sterling
• [Agda] Telescope syntax   Felipe Lessa
• [Agda] Telescope syntax   Andy Morris
• [Agda] Telescope syntax   Matthieu Sozeau
• [Agda] Re: Possible bug when using "with" on a partially applied function   Christopher Jenkins
• [Agda] INTECH 2015 @ Spain   edprocess at dline.info
• [Agda] Telescope syntax   Andreas Abel
• [Agda] Telescope syntax   Guillaume Brunerie
• [Agda] Telescope syntax   Guillaume Brunerie
• [Agda] Telescope syntax   Guillaume Brunerie
• [Agda] Maxime Dene's bug fixed   Thorsten Altenkirch
• [Agda] Telescope syntax   Ulf Norell
• [Agda] Telescope syntax   Guillaume Brunerie
• [Agda] Telescope syntax   Guillaume Brunerie
• [Agda] Maxime Dene's bug fixed   Jesper Cockx
• [Agda] Telescope syntax   Jesper Cockx
• [Agda] Telescope syntax   Guillaume Brunerie
• [Agda] Telescope syntax   Andreas Abel
• [Agda] Telescope syntax   Andreas Abel
• [Agda] Telescope syntax   Jesper Cockx
• [Agda] termination for nested construct   Sergei Meshveliani
• [Agda] Telescope syntax   Guillaume Brunerie
• [Agda] Telescope syntax   Guillaume Brunerie
• [Agda] Telescope syntax   Andreas Abel
• [Agda] Telescope syntax   Nils Anders Danielsson
• [Agda] Telescope syntax   Guillaume Brunerie
• [Agda] Telescope syntax   Guillaume Brunerie
• [Agda] Epic backend question: EpicInclude.e doesn't compile   Hans Peter Würmli
• [Agda] New list agda-dev   Andreas Abel
• [Agda] question about instance arguments   Peter Selinger
• [Agda] question about instance arguments   Dominique Devriese
• [Agda] question about instance arguments   Andreas Abel
• [Agda] question about instance arguments   Andreas Abel
• [Agda] 2 PostDocs in HoTT   Thorsten Altenkirch
• [Agda] question about instance arguments   Peter Selinger
• [Agda] question about instance arguments   Peter Selinger
• [Agda] question about instance arguments   Andreas Abel
• [Agda] question about instance arguments   Peter Selinger
• [Agda] question about instance arguments   Andreas Abel
• [Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...   Dmytro Starosud
• [Agda] question about instance arguments   Peter Selinger
• [Agda] question about instance arguments   Andreas Abel
• [Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...   Andreas Abel
• [Agda] First call for papers LOPSTR 2015 -- 25th International Symposium on Logic-Based Program Synthesis and Transformation -- Siena, Italy   FALASCHI MORENO
• [Agda] PPDP 2015 Call for papers -- 17th International Symposium on Principles and Practice of Declarative Programming -- Siena, Italy   FALASCHI MORENO
• [Agda] question about instance arguments   Roly Perera
• [Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...   Dmytro Starosud
• [Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...   Dmytro Starosud
• [Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...   Dmytro Starosud
• [Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...   Andreas Abel
• [Agda] Poll: maintain support for ghc-7.0 ?!   Andreas Abel
• [Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...   flicky frans
• [Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...   Dmytro Starosud
• [Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...   Dmytro Starosud
• [Agda] Agda and Emacs mode   Andrej Bauer
• [Agda] Agda and Emacs mode   Andrea Vezzosi
• [Agda] Agda and Emacs mode   Andreas Abel
• [Agda] Agda and Emacs mode   Jon Sterling
• [Agda] Agda and Emacs mode   Mateusz Kowalczyk
• [Agda] Agda and Emacs mode   Harley Eades III
• [Agda] Agda and Emacs mode   Mateusz Kowalczyk
• [Agda] CFP: ICADIWT 2015 at Hong Kong   edprocess at dline.info
• [Agda] Epic backend question: EpicInclude.e doesn't compile   Nils Anders Danielsson
• [Agda] Example Runnable Agda Programs   Philipp Hausmann
• [Agda] Example Runnable Agda Programs   Aaron Stump
• [Agda] Example Runnable Agda Programs   Matteo Acerbi
• [Agda] Example Runnable Agda Programs   Alan Jeffrey
• [Agda] Example Runnable Agda Programs   Andreas Abel
• [Agda] Example Runnable Agda Programs   Mateusz Kowalczyk
• [Agda] Example Runnable Agda Programs   Alan Jeffrey
• [Agda] Example Runnable Agda Programs   Sergei Meshveliani
• [Agda] LICS 2015 - Last Call for Papers   Andrzej Murawski
• [Agda] proofs with "with"   Peter Selinger
• [Agda] proofs with "with"   Liam O'Connor
• [Agda] proofs with "with"   Christopher Jenkins
• [Agda] Example Runnable Agda Programs   Ulf Norell
• [Agda] proofs with "with"   Sergei Meshveliani
• [Agda] proofs with "with"   Andrea Vezzosi
• [Agda] proofs with "with"   Wolfram Kahl
• [Agda] Re: proofs with "with"   Stefan Monnier
• [Agda] proofs with "with"   Peter Selinger
• [Agda] Example Runnable Agda Programs   Philipp Hausmann
• [Agda] PhD studentship on Homotopy Type Theory in Nottingham   Thorsten Altenkirch
• [Agda] How can I prove associativity of vectors?   Kenichi Asai
• [Agda] proofs with "with"   Peter Selinger
• [Agda] How can I prove associativity of vectors?   Helmut Grohne
• [Agda] How can I prove associativity of vectors?   Sergei Meshveliani
• [Agda] Re: How can I prove associativity of vectors?   Kenichi Asai
• [Agda] Re: How can I prove associativity of vectors?   Sergei Meshveliani
• [Agda] Re: How can I prove associativity of vectors?   Andreas Abel
• [Agda] Re: How can I prove associativity of vectors?   Kenichi Asai
• [Agda] Re: How can I prove associativity of vectors?   Jon Sterling
• [Agda] Re: How can I prove associativity of vectors?   Andrea Vezzosi
• [Agda] Re: How can I prove associativity of vectors?   Frédéric Blanqui
• [Agda] Re: How can I prove associativity of vectors?   Andrea Vezzosi
• [Agda] Re: How can I prove associativity of vectors?   Frédéric Blanqui
• [Agda] Re: How can I prove associativity of vectors?   Helmut Grohne
• [Agda] Re: How can I prove associativity of vectors?   Andrea Vezzosi
• [Agda] Re: How can I prove associativity of vectors?   Frédéric Blanqui
• [Agda] Re: How can I prove associativity of vectors?   Sergei Meshveliani
• [Agda] Re: How can I prove associativity of vectors?   Sergei Meshveliani
• [Agda] Re: How can I prove associativity of vectors?   Andrea Vezzosi
• [Agda] Re: How can I prove associativity of vectors?   Andreas Abel
• [Agda] How can I prove associativity of vectors?   Conor McBride
• [Agda] How can I prove associativity of vectors?   Conor McBride
• [Agda] CFP: TFPIE 2015   Johan Jeuring
• [Agda] How can I prove associativity of vectors?   Andreas Abel
• [Agda] Re: How can I prove associativity of vectors?   Sergei Meshveliani
• [Agda] Re: How can I prove associativity of vectors?   Sergei Meshveliani
• [Agda] Poll: maintain support for ghc-7.0 ?!   Andrés Sicard-Ramírez
• [Agda] How can I prove associativity of vectors?   Alan Jeffrey
• [Agda] Poll: maintain support for ghc-7.0 ?!   Edward Kmett
• [Agda] Poll: maintain support for ghc-7.0 ?!   Guillaume Brunerie
• [Agda] Poll: maintain support for ghc-7.0 ?!   Andrés Sicard-Ramírez
• [Agda] How can I prove associativity of vectors?   Andrea Vezzosi
• [Agda] How can I prove associativity of vectors?   Dan Licata
• [Agda] How can I prove associativity of vectors?   Alan Jeffrey
• [Agda] termination checking   Peter Selinger
• [Agda] termination checking   Andreas Abel
• [Agda] Poll: maintain support for ghc-7.0 ?!   Andreas Abel
• [Agda] termination checking   Peter Selinger
• Irrelevant termination measure [Re: [Agda] termination checking]   Andreas Abel
• Irrelevant termination measure [Re: [Agda] termination checking]   Gabriel Scherer
• [Agda] [TFP2015] 1st call for papers   Peter Achten
• Irrelevant termination measure [Re: [Agda] termination checking]   Andreas Abel
• [Agda] PhD studentship on dependent type theory for concurrent processes   Martin Berger
• [Agda] Inspect.   flicky frans
• [Agda] `postulate' under `with'   Sergei Meshveliani
• [Agda] `postulate' under `with'   flicky frans
• [Agda] Inspect.   Andreas Abel
• [Agda] Agda student's research   Peter Divianszky
• [Agda] Inspect.   flicky frans
• [Agda] Inspect.   Andreas Abel
• [Agda] Inspect.   Andrés Sicard-Ramírez
• [Agda] Inspect.   Aaron Stump
• [Agda] Inspect.   flicky frans
• [Agda] Inspect.   Andreas Abel
• [Agda] Inspect.   flicky frans
• [Agda] Agda student's research   Sergei Meshveliani
• [Agda] with x =? x   Sergei Meshveliani
• [Agda] with x =? x   Andrea Vezzosi
• [Agda] with x =? x   Sergei Meshveliani
• [Agda] with x=?x   Wolfram Kahl
• [Agda] with x =? x   Andrea Vezzosi

Last message date: Wed Dec 31 23:43:22 CEST 2014
Archived on: Wed Dec 31 23:43:25 CEST 2014

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