2016 Archives by date

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

Starting: Fri Jan 1 06:39:22 CET 2016
Ending: Fri Dec 30 16:02:40 CET 2016
Messages: 802

• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to include Data.List without conflict with agda-prelude   Mandy Martino
• [Agda] how to include Data.List without conflict with agda-prelude   Ulf Norell
• [Agda] command line type checker vs interactive   Sergei Meshveliani
• [Agda] command line type checker vs interactive   Sergei Meshveliani
• [Agda] command line type checker vs interactive   Sergei Meshveliani
• [Agda] how to include Data.List without conflict with agda-prelude   Mandy Martino
• [agda] agda2-mode not found and further errors   Mandy Martino
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] No binding for builtin thing IO, use {-# BUILTIN IO name #-} to bind it to 'name'   Mandy Martino
• [Agda] how to include Data.List without conflict with agda-prelude   Ulf Norell
• [Agda] how to include Data.List without conflict with agda-prelude   Mandy Martino
• [Agda] how to include Data.List without conflict with agda-prelude   Andrés Sicard-Ramírez
• [Agda] sharing a variable in a with clause and its result   Kenichi Asai
• [Agda] how to include Data.List without conflict with agda-prelude   Mandy Martino
• [Agda] is Agda 1 and Agda 2 are different things   Mandy Martino
• [Agda] command line type checker vs interactive   Nils Anders Danielsson
• [agda] agda2-mode not found and further errors   Nils Anders Danielsson
• [Agda] is Agda 1 and Agda 2 are different things   Nils Anders Danielsson
• [Agda] sharing a variable in a with clause and its result   Nils Anders Danielsson
• [Agda] sharing a variable in a with clause and its result   effectfully
• [Agda] is Agda 1 and Agda 2 are different things   Mandy Martino
• [Agda] MSFP 2016: Call for Papers   Bob Atkey
• [Agda] Generic Programming with Indexed Functors   Martin Stone Davis
• [Agda] Generic Programming with Indexed Functors   Andrea Vezzosi
• [Agda] Generic Programming with Indexed Functors   Thorsten Altenkirch
• [Agda] is Agda 1 and Agda 2 are different things   Nils Anders Danielsson
• [Agda] Is it possible to switch off universes checking?   Andreas Abel
• [Agda] No binding for builtin thing IO, use {-# BUILTIN IO name #-} to bind it to 'name'   Andreas Abel
• [Agda] installing Dev Agda Jan-9   Sergei Meshveliani
• [Agda] Bug in Development Jan-9 ?   Sergei Meshveliani
• [Agda] Bug in Development Jan-9 ?   Sergei Meshveliani
• [Agda] Is it possible to switch off universes checking?   effectfully
• [Agda] missing double definition   Sergei Meshveliani
• [Agda] missing double definition   Andreas Abel
• [Agda] MSFP 2016: Final Call for Papers   Bob Atkey
• [Agda] Agda reflection overhaul   Ulf Norell
• [Agda] Re: Agda reflection overhaul   Jesper Cockx
• [Agda] Re: Agda reflection overhaul   Ulf Norell
• [Agda] Re: Agda reflection overhaul   David Raymond Christiansen
• [Agda] Google Summer of Code Projects   Martin Bidlingmaier
• [Agda] How to solve goals that involve a vertical bar?   Martin Stone Davis
• [Agda] Re: How to solve goals that involve a vertical bar?   Martin Stone Davis
• [Agda] Re: How to solve goals that involve a vertical bar?   Martin Stone Davis
• [Agda] Re: How to solve goals that involve a vertical bar?   Martin Stone Davis
• [Agda] Re: How to solve goals that involve a vertical bar?   Martin Stone Davis
• [Agda] rewrite on the right?   Martin Stone Davis
• [Agda] rewrite on the right?   Andrea Vezzosi
• [Agda] rewrite on the right?   Jesper Cockx
• [Agda] [agda2] how to programming the basic   Mandy Martino
• [Agda] rewrite on the right?   Victor Miraldo
• [Agda] [agda2] how to programming the basic   mechvel at scico.botik.ru
• [Agda] [new-reflection] unsolved metas in induction   Martin Stone Davis
• [Agda] [new-reflection] unsolved metas in induction   Ulf Norell
• [Agda] [agda2] how to programming the basic   Mandy Martino
• [Agda] [agda2] how to programming the basic   Andreas Abel
• [Agda] [agda2] how to programming the basic   Mandy Martino
• [Agda] [agda2] how to programming the basic   Sergei Meshveliani
• [Agda] [agda2] how to programming the basic   Mandy Martino
• [Agda] [agda2] how to programming the basic   Mandy Martino
• [Agda] [agda2] how to programming the basic   Andreas Abel
• [Agda] [agda2] how to programming the basic   Sergei Meshveliani
• [Agda] Re: Generic Programming with Indexed Functors   Kenichi Asai
• [Agda] Call for participation: Agda Implementors' Meeting XXIII at Strathclyde, 20--26 April 2016   Fredrik Nordvall Forsberg
• [Agda] Re: Generic Programming with Indexed Functors   Martin Stone Davis
• [Agda] [agda2] how to programming the basic   Mandy Martino
• [Agda] [agda2] how to programming the basic   Sergei Meshveliani
• [Agda] aggressive with, VFPiA   Aaron Stump
• [Agda] Rewriting in general   Owen
• rewrite and issue 1692 [Re: [Agda] aggressive with, VFPiA]   Andreas Abel
• rewrite and issue 1692 [Re: [Agda] aggressive with, VFPiA]   Aaron Stump
• rewrite and issue 1692 [Re: [Agda] aggressive with, VFPiA]   Andreas Abel
• rewrite and issue 1692 [Re: [Agda] aggressive with, VFPiA]   Aaron Stump
• [Agda] is there a show function like haskell to show result of a running function   Mandy Martino
• [Agda] is Category directory in agda-std library a complete version?   Mandy Martino
• [Agda] Re: Agda reflection overhaul   Ulf Norell
• rewrite and issue 1692 [Re: [Agda] aggressive with, VFPiA]   Nils Anders Danielsson
• rewrite and issue 1692 [Re: [Agda] aggressive with, VFPiA]   Andreas Abel
• [Agda] is there a show function like haskell to show result of a running function   Sergei Meshveliani
• [Agda] is there a show function like haskell to show result of a running function   Nils Anders Danielsson
• [Agda] Re: about RingSolver   Sergei Meshveliani
• [Agda] Re: about RingSolver   Nils Anders Danielsson
• [Agda] is there a show function like haskell to show result of a running function   Sergei Meshveliani
• [Agda] is there a show function like haskell to show result of a running function   Nils Anders Danielsson
• [Agda] FSCD'16 deadline extension   Andreas Abel
• [Agda] effect of skipping `module'   Sergei Meshveliani
• [Agda] Expose more of Agda to reflection?   Martin Stone Davis
• [Agda] Type-checker evaluator performance   Liam O'Connor
• [Agda] Type-checker evaluator performance   Andrea Vezzosi
• [Agda] effect of skipping `module'   Andreas Abel
• [Agda] Type-checker evaluator performance   Peter Selinger
• [Agda] Expose more of Agda to reflection?   Jesper Cockx
• [Agda] Type-checker evaluator performance   Liam O'Connor
• [Agda] Type-checker evaluator performance   effectfully
• [Agda] Type-checker evaluator performance   Liam O'Connor
• [Agda] Type-checker evaluator performance   effectfully
• [Agda] Type-checker evaluator performance   Liam O'Connor
• [Agda] Type-checker evaluator performance   Wolfram Kahl
• [Agda] Type-checker evaluator performance   Liam O'Connor
• [Agda] Type-checker evaluator performance   Liam O'Connor
• [Agda] Type-checker evaluator performance   Liam O'Connor
• [Agda] effect of skipping `module'   Andreas Abel
• [Agda] pattern match for LessThan'?   Kenichi Asai
• [Agda] Type-checker evaluator performance   Dominique Devriese
• [Agda] Type-checker evaluator performance   Jon Sterling
• [Agda] [TFP 2016] 1st call for papers   Peter Achten
• [Agda] pattern match for LessThan'?   Martin Stone Davis
• [Agda] Re: pattern match for LessThan'?   Kenichi Asai
• [Agda] Expose more of Agda to reflection?   Thorsten Altenkirch
• [Agda] Re: pattern match for LessThan'?   Andreas Abel
• [Agda] Re: pattern match for LessThan'?   Nils Anders Danielsson
• [Agda] Expose more of Agda to reflection?   Martin Stone Davis
• [Agda] Expose more of Agda to reflection?   Ulf Norell
• [Agda] Type-checker evaluator performance   Ulf Norell
• [Agda] Type-checker evaluator performance   Jacques Carette
• [Agda] Type-checker evaluator performance   Sergei Meshveliani
• [Agda] Type-checker evaluator performance   Ulf Norell
• [Agda] Type-checker evaluator performance   Ulf Norell
• [Agda] Type-checker evaluator performance   Nils Anders Danielsson
• [Agda] Type-checker evaluator performance   Jacques Carette
• [Agda] Type-checker evaluator performance   Liam O'Connor
• [Agda] Workshop on Homotopy Type Theory and Univalent Foundations, Fields Institute, May 16-20, 2016   Chris Kapulkin
• [Agda] Type-checker evaluator performance   Sergei Meshveliani
• [Agda] more on type check performance   Sergei Meshveliani
• [Agda] Type-checker evaluator performance   Nils Anders Danielsson
• [Agda] Rewriting in general   Nils Anders Danielsson
• [Agda] Efficiency of type checking   Thorsten Altenkirch
• [Agda] A quiz: what should the types of these definitions be?   Andreas Abel
• [Agda] A quiz: what should the types of these definitions be?   Nils Anders Danielsson
• [Agda] "xs ≡ [] → " question   Sergei Meshveliani
• [Agda] A quiz: what should the types of these definitions be?   Andreas Abel
• Re: [Agda] "xs ≡ [] → " question   Jesper Cockx
• [Agda] Type-checker evaluator performance   Liam O'Connor
• Re: [Agda] "xs ≡ [] → " question   effectfully
• [Agda] A quiz: what should the types of these definitions be?   Ulf Norell
• Re: [Agda] "xs ≡ [] → " question   Andreas Abel
• [Agda] A quiz: what should the types of these definitions be?   Andreas Abel
• [Agda] A quiz: what should the types of these definitions be?   Ulf Norell
• [Agda] A quiz: what should the types of these definitions be?   Andreas Abel
• [Agda] Type-checker evaluator performance   Peter Selinger
• [Agda] "xs ≡ [] → " question   Sergei Meshveliani
• [Agda] "xs ≡ [] → " question   Sergei Meshveliani
• [Agda] `with' question   Sergei Meshveliani
• [Agda] `with' question   Martin Stone Davis
• [Agda] A quiz: what should the types of these definitions be?   Wolfram Kahl
• [Agda] how to run this rewrite example   Mandy Martino
• [Agda] `with' question   Sergei Meshveliani
• [Agda] how to run this rewrite example   Martin Stone Davis
• [Agda] Running the TC monad   Yorick Sijsling
• [Agda] Running the TC monad   Ulf Norell
• [Agda] Running the TC monad   Yorick Sijsling
• [Agda] ICFP 2016 Second Call for Papers   Lindsey Kuper
• [Agda] `with' question   Andreas Abel
• [Agda] rewrite on the right?   Martin Stone Davis
• [Agda] [ANNOUNCE] Agda 2.5.1 release candidate   Andrés Sicard-Ramírez
• [Agda] sym in Agda 2.5.1   John Leo
• [Agda] [ANNOUNCE] Agda 2.5.1 release candidate   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.1 release candidate   Andreas Abel
• [Agda] [ANNOUNCE] Agda 2.5.1 release candidate   Philipp Hausmann
• [Agda] testing 2.5 candidate   Sergei Meshveliani
• [Agda] testing 2.5 candidate   Andrés Sicard-Ramírez
• [Agda] Re: [ANNOUNCE] Agda 2.5.1 release candidate   darais at cs.umd.edu
• [Agda] Re: [ANNOUNCE] Agda 2.5.1 release candidate   Ulf Norell
• [Agda] sym in Agda 2.5.1   Andrés Sicard-Ramírez
• [Agda] sym in Agda 2.5.1   Andrés Sicard-Ramírez
• [Agda] sym in Agda 2.5.1   John Leo
• [Agda] sym in Agda 2.5.1   Andrea Vezzosi
• [Agda] sym in Agda 2.5.1   Andrés Sicard-Ramírez
• [Agda] sym in Agda 2.5.1   John Leo
• [Agda] sym in Agda 2.5.1   John Leo
• [Agda] sym in Agda 2.5.1   Andrés Sicard-Ramírez
• [Agda] sym in Agda 2.5.1   Andrés Sicard-Ramírez
• [Agda] sym in Agda 2.5.1   Andrea Vezzosi
• [Agda] [TFPIE 2016] 1st call for papers   Peter Achten
• [Agda] sym in Agda 2.5.1   Andrés Sicard-Ramírez
• [Agda] Version of the standard library compatible with Agda 2.5.1 release candidate 1   Andrés Sicard-Ramírez
• [Agda] Another potential typeclass bug in release-candidate/master   David Darais
• [Agda] Another potential typeclass bug in release-candidate/master   Ulf Norell
• [Agda] PrlConf CFP: Structural and Behavioral Foundations of Programming Languages   Jon Sterling
• [Agda] Another potential typeclass bug in release-candidate/master   David Darais
• [Agda] rewrite on the right?   Martin Stone Davis
• [Agda] Another potential typeclass bug in release-candidate/master   Ulf Norell
• [Agda] Typeclasses again in release-candidate/master   David Darais
• [Agda] Typeclasses again in release-candidate/master   Ulf Norell
• [Agda] Typeclasses again in release-candidate/master   effectfully
• [Agda] Typeclasses again in release-candidate/master   Ulf Norell
• [Agda] Typeclasses again in release-candidate/master   Andrea Vezzosi
• [Agda] Typeclasses again in release-candidate/master   David Darais
• [Agda] Typeclasses again in release-candidate/master   Andreas Abel
• [Agda] Typeclasses again in release-candidate/master   Ulf Norell
• [Agda] Typeclasses again in release-candidate/master   Andrea Vezzosi
• [Agda] [reright] debugging unsolved metas in a nested tactic   Martin Stone Davis
• [Agda] Re: [reright] debugging unsolved metas in a nested tactic   Martin Stone Davis
• [Agda] Re: [reright] debugging unsolved metas in a nested tactic   Ulf Norell
• [Agda] Re: [reright] debugging unsolved metas in a nested tactic   Martin Stone Davis
• [Agda] inferType yields a metavariable   Martin Stone Davis
• [Agda] inferType yields a metavariable   Ulf Norell
• [Agda] inferType yields a metavariable   Martin Stone Davis
• [Agda] inferType yields a metavariable   Ulf Norell
• [Agda] inferType yields a metavariable   Martin Stone Davis
• [Agda] Call for Participation: MSFP 2016   Bob Atkey
• [Agda] inferType yields a metavariable   Ulf Norell
• [Agda] inferType yields a metavariable   Martin Stone Davis
• [Agda] rewrite on the right?   Martin Stone Davis
• [Agda] about `abstract'   Sergei Meshveliani
• [Agda] about `abstract'   Sergei Meshveliani
• [Agda] about `abstract'   Ulf Norell
• [Agda] about `abstract'   Sergei Meshveliani
• [Agda] announcing Verified Functional Programming in Agda   Aaron Stump
• [Agda] announcing Verified Functional Programming in Agda   Harley Eades III
• [Agda] announcing Verified Functional Programming in Agda   Jon Sterling
• [Agda] [TFP 2016] 2nd call for papers   Peter Achten
• [Agda] Komencenta demando.   Serge Leblanc
• [Agda] about `abstract'   Ulf Norell
• [Agda] Komencenta demando.   Matteo Acerbi
• [Agda] Backus–Naur Form    
• [Agda] ICFP 2016 Final Call for Papers   Lindsey Kuper
• [Agda] One more time about Backus-Naur form    
• [Agda] about `abstract'   Sergei Meshveliani
• [Agda] about `abstract'   Ulf Norell
• [Agda] Re: Backus-Naur form   Sergei Meshveliani
• [Agda] about `abstract'   Sergei Meshveliani
• [Agda] "Hiding of record parameters"   Sergei Meshveliani
• [Agda] "Hiding of record parameters"   Andrés Sicard-Ramírez
• [Agda] Komencenta demando.   Thorsten Altenkirch
• [Agda] One more time about Backus-Naur form   Guillaume Brunerie
• [Agda] Problem with \lambda    
• [Agda] Problem with \lambda   Nils Anders Danielsson
• [Agda] "Hiding of record parameters leads ..."   Sergei Meshveliani
• [Agda] Slow type-checking of records   Andreas Nuyts
• [Agda] Problem with \lambda   Andreas Abel
• [Agda] Slow type-checking of records   Andreas Abel
• [Agda] Slow type-checking of records   Nils Anders Danielsson
• [Agda] Call for participation: Agda Implementors' Meeting XXIII at Strathclyde, 20--26 April 2016   James Chapman
• [Agda] Slow type-checking of records   Sergei Meshveliani
• [Agda] Call for participation: Agda Implementors' Meeting XXIII at Strathclyde, 20--26 April 2016   James Chapman
• [Agda] Slow type-checking of records   Andreas Nuyts
• [Agda] Slow type-checking of records   Wolfram Kahl
• [Agda] Slow type-checking of records   Andrea Vezzosi
• [Agda] Slow type-checking of records   Nils Anders Danielsson
• [Agda] CfP: UF/HoTT workshop, Porto, 25--26 June, with FSCD 2016   Peter LeFanu Lumsdaine
• [Agda] Slow type-checking of records   Nils Anders Danielsson
• [Agda] heres a nice example of copattern matching   Carter Schonwald
• [Agda] Induction-induction in a tricky order   Simon Boulier
• [Agda] Induction-induction in a tricky order   Dr. ERDI Gergo
• [Agda] Induction-induction in a tricky order   Dr. ERDI Gergo
• [Agda] Induction-induction in a tricky order   Simon Boulier
• [Agda] Induction-induction in a tricky order   Jesper Cockx
• [Agda] Induction-induction in a tricky order   Fredrik Nordvall Forsberg
• [Agda] Induction-induction in a tricky order   Simon Boulier
• [Agda] Induction-induction in a tricky order   Thorsten Altenkirch
• [Agda] Induction-induction in a tricky order   Nils Anders Danielsson
• [Agda] Slow type-checking of records   Nils Anders Danielsson
• [Agda] Slow type-checking of records   Jesper Cockx
• [Agda] Slow type-checking of records   Carter Schonwald
• [Agda] Slow type-checking of records   Carter Schonwald
• [Agda] Call for Bids to Host ITP 2017   Nils Anders Danielsson
• [Agda] Slow type-checking of records   Dominique Devriese
• [Agda] IAL 1.3 for Agda 2.5.1   Aaron Stump
• [Agda] Slow type-checking of records   Carter Schonwald
• [Agda] Call for Papers: Workshop on User Interfaces for Theorem Provers (UITP 2016 @ IJCAR), Coimbra, Portugal, Deadline May 9th   Serge Autexier
• [Agda] CFP: Workshop on Type-driven Development (TyDe '16)   Wouter Swierstra
• [Agda] [TFPIE 2016] 2nd call for papers   Peter Achten
• [Agda] ICMS 2016   Vladimir Voevodsky
• [Agda] Priority of infix and prefix constructors    
• [Agda] Agda Proofs for Harper's Practical Foundations of Programming Languages   Shin-Cheng Mu
• [Agda] termination proof problem   Sergei Meshveliani
• [Agda] termination proof problem   Sergei Meshveliani
• [Agda] termination proof problem   Andrea Vezzosi
• [Agda] termination proof problem   Sergei Meshveliani
• [Agda] termination proof problem   Andrea Vezzosi
• [Agda] termination proof problem   Andrea Vezzosi
• [Agda] termination proof problem   Sergei Meshveliani
• [Agda] termination proof problem   Sergei Meshveliani
• [Agda] Users of --no-coverage-check !?   Andreas Abel
• [Agda] Priority of infix and prefix constructors   Andreas Abel
• [Agda] termination proof problem   Ulf Norell
• [Agda] termination proof problem   Sergei Meshveliani
• [Agda] Hammers for Type Theories: Second Call for Papers   Jasmin Blanchette
• [Agda] Allow certain whitespace characters in identifiers   David Raymond Christiansen
• [Agda] [TFP 2016] Final call for papers   Peter Achten
• [Agda] Allow certain whitespace characters in identifiers   Andreas Abel
• [Agda] Allow certain whitespace characters in identifiers   Peter Hancock
• [Agda] Re: Call for participation: Agda Implementors' Meeting XXIII at Strathclyde, 20--26 April 2016   Fredrik Nordvall Forsberg
• [Agda] beamer + latex mode + font sizes   Jacques Carette
• [Agda] Autumn school "Proof and Computation"   Kenji Miyamoto
• [Agda] Journal of Functional Programming - Call for PhD Abstracts   Graham Hutton
• [Agda] beamer + latex mode + font sizes   Andrés Sicard-Ramírez
• [Agda] beamer + latex mode + font sizes   Jacques Carette
• [Agda] Komencanta demando.   Serge Leblanc
• [Agda] Komencanta demando.   Andreas Abel
• [Agda] Workshop on Categorical Logic and Univalent Foundations   Christian Sattler
• [Agda] Komencanta demando.   Martin Stone Davis
• [Agda] Komencanta demando.   Martin Stone Davis
• [Agda] `let' and `case'   Sergei Meshveliani
• [Agda] `let' and `case'   Andreas Abel
• [Agda] uniform normalization   Sergei Meshveliani
• [Agda] uniform normalization   Andreas Abel
• [Agda] uniform normalization   Andrew Pitts
• [Agda] uniform normalization   Bradley Hardy
• [Agda] uniform normalization   Ulf Norell
• [Agda] [TFP 2016] extended deadline, april 25 2016, final call for papers   Peter Achten
• [Agda] Second CfP: UF/HoTT Porto, 25--26 June, at FSCD 2016   Peter LeFanu Lumsdaine
• [Agda] [ANNOUNCE] Agda 2.5.1 release candidate 2   Andrés Sicard-Ramírez
• [Agda] Re: [ANNOUNCE] Agda 2.5.1 release candidate 2   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.1 release candidate 2   Sergei Meshveliani
• [Agda] LC2016: approaching deadlines   Nicola Gambino
• [Agda] [ANNOUNCE] Agda 2.5.1 release candidate 2   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.1 release candidate 2   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.1 release candidate 2   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.1 release candidate 2   Wolfram Kahl
• [Agda] Re: [ANNOUNCE] Agda 2.5.1 release candidate 2   Andrés Sicard-Ramírez
• [Agda] Haskell cost centers?   Aaron Stump
• [Agda] Haskell cost centers?   Wolfram Kahl
• [Agda] Haskell cost centers?   Aaron Stump
• [Agda] Inteligenta tipa kontrolilo?   Serge Leblanc
• [Agda] Inteligenta tipa kontrolilo?   David Christiansen
• [Agda] [ANNOUNCE] Agda 2.5.1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Standard library 0.12   Andrés Sicard-Ramírez
• [Agda] Inteligenta tipa kontrolilo?   Martin Stone Davis
• [Agda] Inteligenta tipa kontrolilo?   Ulf Norell
• [Agda] Inteligenta tipa kontrolilo?   Serge Leblanc
• [Agda] Inteligenta tipa kontrolilo?   Serge Leblanc
• [Agda] Haskell cost centers?   Andreas Abel
• [Agda] Inteligenta tipa kontrolilo?   Serge Leblanc
• [Agda] Inteligenta tipa kontrolilo?   David Raymond Christiansen
• [Agda] Generic programming via effects   Roman
• [Agda] [ANNOUNCE] Agda 2.5.1   Andrew Pitts
• [Agda] [ANNOUNCE] Agda 2.5.1   Bradley Hardy
• [Agda] [ANNOUNCE] Agda 2.5.1   Andrew Pitts
• Agda refers to things not in scope [Re: [Agda] [ANNOUNCE] Agda 2.5.1]   Andreas Abel
• [Agda] [ANNOUNCE] Agda 2.5.1   Thorsten Altenkirch
• Fwd: Agda refers to things not in scope [Re: [Agda] [ANNOUNCE] Agda 2.5.1]   Andrew Pitts
• [Agda] [ANNOUNCE] Agda 2.5.1   Andrew Pitts
• [Agda] Inteligenta tipa kontrolilo?   Serge Leblanc
• [Agda] [ANNOUNCE] Agda 2.5.1   Andrew Pitts
• [Agda] [ANNOUNCE] Agda 2.5.1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.1   Harley Eades III
• [Agda] [ANNOUNCE] Agda 2.5.1   Ulf Norell
• [Agda] [ANNOUNCE] Agda 2.5.1   Andrew Pitts
• [Agda] [ANNOUNCE] Agda 2.5.1   Ulf Norell
• [Agda] [ANNOUNCE] Agda 2.5.1   Andrew Pitts
• [Agda] The 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP'17)   Ana Bove
• [Agda] Ph.D. Position in Security Modeling at IRISA in Rennes, France   Barbara Kordy
• [Agda] [ANNOUNCE] Agda 2.5.1   Thorsten Altenkirch
• [Agda] [ANNOUNCE] Agda 2.5.1   Ulf Norell
• [Agda] [ANNOUNCE] Agda 2.5.1   Thorsten Altenkirch
• [Agda] [ANNOUNCE] Agda 2.5.1   Roman
• [Agda] [ANNOUNCE] Agda 2.5.1   John Leo
• [Agda] [ANNOUNCE] Agda 2.5.1   Thorsten Altenkirch
• [Agda] Re: Agda Digest, Vol 127, Issue 17   Keith Ramsay
• [Agda] Accidental reply   Keith Ramsay
• [Agda] Baza Agda progamo skribita per Agda ?   Serge Leblanc
• [Agda] [ANNOUNCE] Agda 2.5.1   Nils Anders Danielsson
• [Agda] [ANNOUNCE] Agda 2.5.1   John Leo
• [Agda] 1st CFP: SLE 2016 (9th ACM SIGPLAN International Conference on Software Language Engineering)   Andrei Chis
• [Agda] Summer School on Bidirectional Transformations, Oxford, 25-29th July 2016   Jeremy.Gibbons at cs.ox.ac.uk
• [Agda] [TFP'16] call for participation   Peter Achten
• [Agda] double constructor termination   Sergei Meshveliani
• [Agda] double constructor termination   Jesper Cockx
• [Agda] Re: double constructor termination   Sergei Meshveliani
• [Agda] list head eq   Sergei Meshveliani
• [Agda] list head eq   Bradley Hardy
• [Agda] double constructor termination   Andreas Abel
• [Agda] double constructor termination   Andreas Abel
• [Agda] `with' to case_of_ example   Sergei Meshveliani
• [Agda] Add Agda papers to the wiki   Nils Anders Danielsson
• [Agda] Last Call for Papers: Workshop on User Interfaces for Theorem Provers (UITP 2016 @ IJCAR), Coimbra, Portugal, Deadline May 17th *NEW* (was May 9th, 2016)   Serge Autexier
• [Agda] `with' to case_of_ example   Sergei Meshveliani
• [Agda] `with' to case_of_ example   Andreas Abel
• [Agda] Stranga konduto !   Serge Leblanc
• [Agda] Stranga konduto !   Roman
• [Agda] Stranga konduto !   G. Allais
• [Agda] `with' to case_of_ example   Thorsten Altenkirch
• [Agda] Call to Vote on Bids to Host ITP 2017   Jasmin Blanchette
• [Agda] 2-year postdoctoral position in programming languages at LFCS   James Cheney
• [Agda] Add Agda papers to the wiki   Andreas Abel
• [Agda] `with' to case_of_ example   Sergei Meshveliani
• [Agda] Trustworthy Refactoring project: Research Associate Positions in Refactoring Functional Programs and Formal Verification (for CakeML)   Simon Thompson
• [Agda] Not Unfolding Local Defs   Harley Eades III
• [Agda] Not Unfolding Local Defs   Andrés Sicard-Ramírez
• [Agda] Not Unfolding Local Defs   Harley D. Eades III
• [Agda] Not Unfolding Local Defs   G. Allais
• [Agda] Not Unfolding Local Defs   Jon Sterling
• [Agda] Not Unfolding Local Defs   Harley Eades III
• [Agda] Not Unfolding Local Defs   Harley Eades III
• [Agda] Not Unfolding Local Defs   Wouter Swierstra
• [Agda] Not Unfolding Local Defs   Yorick Sijsling
• [Agda] stuck with "unsolved metas"   Sergei Meshveliani
• [Agda] AoPA -- Algebra of Programming in Agda (updated 2016)   Shin-Cheng Mu
• [Agda] stuck with "unsolved metas"   Andreas Abel
• [Agda] stuck with "unsolved metas"   Sergei Meshveliani
• [Agda] stuck with "unsolved metas"   Roman
• [Agda] unicode input   Martin Escardo
• [Agda] stuck with "unsolved metas"   Andreas Abel
• [Agda] unicode input   Nils Anders Danielsson
• [Agda] stuck with "unsolved metas"   Sergei Meshveliani
• [Agda] stuck with "unsolved metas"   Roman
• [Agda] stuck with "unsolved metas"   Andreas Abel
• [Agda] stuck with "unsolved metas"   Sergei Meshveliani
• [Agda] Re: unicode input   Stefan Monnier
• [Agda] Komencanta demando.   Serge Leblanc
• [Agda] PLRR 2017 (Parametricity, Logical Relations & Realizability), call for contribution   Pierre Hyvernat
• [Agda] 1st CfP: IFL 2016 (28th Symposium on Implementation and Application of Functional Languages)   publicityifl at gmail.com
• [Agda] CFP: Workshop on Type-driven Development (TyDe '16)   Wouter Swierstra
• [Agda] Not Unfolding Local Defs   Harley Eades III
• [Agda] postdoc recruiting   Aaron Stump
• [Agda] Re: postdoc recruiting   Aaron Stump
• [Agda] SIGPLAN Programming Languages Mentoring Workshop @ ICFP   Lindsey Kuper
• [Agda] 2nd CfP: SLE 2016 (9th ACM SIGPLAN International Conference on Software Language Engineering)   Andrei Chis
• [Agda] References to the "old" ways of installing the agda stdlib   Jesper Louis Andersen
• [Agda] References to the "old" ways of installing the agda stdlib   Miëtek Bak
• [Agda] References to the "old" ways of installing the agda stdlib   Nils Anders Danielsson
• [Agda] References to the "old" ways of installing the agda stdlib   Natalie Perna
• [Agda] Markov's principle   Sergei Meshveliani
• [Agda] Markov's principle   Sergei Meshveliani
• [Agda] Workshop on Categorical Logic and Univalent Foundations: Deadline Approaching   Christian Sattler
• [Agda] References to the "old" ways of installing the agda stdlib   Ulf Norell
• [Agda] References to the "old" ways of installing the agda stdlib   Ulf Norell
• [Agda] Upcoming feature: Postfix projections   Andreas Abel
• [Agda] adapting Agda for next-gen blockchain apps   Ren Rise
• [Agda] What is wrong about this proof for A ⊆ A ∪ B   Katsutoshi Itoh
• Re: [Agda] What is wrong about this proof for A ⊆ A ∪ B   Andreas Abel
• [Agda] adapting Agda for next-gen blockchain apps   Ren Rise
• [Agda] adapting Agda for next-gen blockchain apps   Andreas Abel
• [Agda] [ANNOUNCE] Agda 2.5.1.1 release candidate 1   Ulf Norell
• Re: [Agda] What is wrong about this proof for A ⊆ A ∪ B   Katsutoshi Itoh
• [Agda] not able to run Agda on Haskell and Emac and a relevant hypercomputing question   Ren Rise
• [Agda] not able to run Agda on Haskell and Emac and a relevant hypercomputing question   Andreas Abel
• [Agda] Confusion with levels in proof irrelevance   Jan Bracker
• [Agda] Confusion with levels in proof irrelevance   Andreas Abel
• [Agda] Reflection: type-definition vs. getType and getDefinitions functions.   Ernesto Copello
• [Agda] Reflection: type-definition vs. getType and getDefinitions functions.   Ulf Norell
• [Agda] A feature request: typed pattern synonyms.   Roman
• [Agda] expections while running Agda on Windows 10 with MingGW MSYS and Cygwin   Ren Rise
• [Agda] expections while running Agda on Windows 10 with MingGW MSYS and Cygwin   Andreas Abel
• [Agda] expections while running Agda on Windows 10 with MingGW MSYS and Cygwin   Andrés Sicard-Ramírez
• [Agda] exceptions while running Agda on Windows 10 with MingGW MSYS and Cygwin   Ren Rise
• [Agda] A feature request: typed pattern synonyms.   Yorick Sijsling
• [Agda] factorization monoid, ring   Sergei Meshveliani
• [Agda] factorization monoid, ring   Sergei Meshveliani
• [Agda] A feature request: typed pattern synonyms.   Roman
• [Agda] exceptions while running Agda on Windows 10 with MingGW MSYS and Cygwin   Roman
• [Agda] exceptions while running Agda on Windows 10 with MingGW MSYS and Cygwin   Andrés Sicard-Ramírez
• [Agda] exceptions while running Agda on Windows 10 with MingGW MSYS and Cygwin   Andrés Sicard-Ramírez
• [Agda] excluded-middle   Katsutoshi Itoh
• [Agda] excluded-middle   Martin Escardo
• [Agda] factorization monoid, ring   Andreas Abel
• [Agda] exceptions while running Agda on Windows 10 with MingGW MSYS and Cygwin   Andreas Abel
• [Agda] exceptions while running Agda on Windows 10 with MingGW MSYS and Cygwin   Andrés Sicard-Ramírez
• [Agda] exceptions while running Agda on Windows 10 with MingGW MSYS and Cygwin   Ulf Norell
• [Agda] excluded-middle   Nils Anders Danielsson
• [Agda] factorization monoid, ring   N. Raghavendra
• [Agda] excluded-middle   Martín Hötzel Escardó
• [Agda] WFLP 2016 - Final Call for Papers   Janis Voigtlaender
• [Agda] ITP 2016: Call for participation   Jasmin Blanchette
• [Agda] Programming in Haskell - 2nd Edition   Graham Hutton
• [Agda] [ANNOUNCE] Agda 2.5.1.1   Andrés Sicard-Ramírez
• [Agda] help required for installing GHC or whole Haskell platform   Ren Rise
• [Agda] factorization monoid, ring   Sergei Meshveliani
• [Agda] help required for installing GHC or whole Haskell platform   Andrés Sicard-Ramírez
• [Agda] help required for installing GHC or whole Haskell platform   Andrés Sicard-Ramírez
• [Agda] excluded-middle   Katsutoshi Itoh
• [Agda] help required for installing GHC or whole Haskell platform   Ren Rise
• [Agda] help required for installing GHC or whole Haskell platform   Ren Rise
• [Agda] excluded-middle   Nils Anders Danielsson
• [Agda] help required for installing GHC or whole Haskell platform   Nils Anders Danielsson
• [Agda] excluded-middle   Thorsten Altenkirch
• [Agda] excluded-middle   Owen
• [Agda] help required for installing GHC or whole Haskell platform   ren.rise at gmx.com
• [Agda] help required for installing GHC or whole Haskell platform   Andrés Sicard-Ramírez
• [Agda] help required for installing GHC or whole Haskell platform   Ren Rise
• [Agda] help required for installing GHC or whole Haskell platform   Andrés Sicard-Ramírez
• [Agda] help required for installing GHC or whole Haskell platform   Andrés Sicard-Ramírez
• Fw: Re: Re: [Agda] help required for installing GHC or whole Haskell platform   Ren Rise
• [Agda] help required for installing GHC or whole Haskell platform   Andreas Abel
• [Agda] help required for installing GHC or whole Haskell platform   Ulf Norell
• [Agda] PEPM 2017 Call for Papers   Jeremy Yallop
• [Agda] help required for installing GHC or whole Haskell platform   Ren Rise
• [Agda] help required for installing GHC or whole Haskell platform   Ren Rise
• [Agda] help required for installing GHC or whole Haskell platform   Wolfram Kahl
• [Agda] excluded-middle   Katsutoshi Itoh
• [Agda] Formalization of Linear Algebra in agda   Guillermo Calderon
• [Agda] A feature request: typed pattern synonyms.   Andreas Abel
• [Agda] Formalization of Linear Algebra in agda   Sergei Meshveliani
• [Agda] 2nd CfP: IFL 2016 (28th Symposium on Implementation and Application of Functional Languages)   publicityifl at gmail.com
• [Agda] origin of "Agda"?   Peter Selinger
• [Agda] origin of "Agda"?   John Leo
• [Agda] origin of "Agda"?   Vilhelm Sjoberg
• [Agda] origin of "Agda"?   Andreas Abel
• [Agda] origin of "Agda"?   Peter Selinger
• [Agda] origin of "Agda"?   Miëtek Bak
• [Agda] Re: Formalization of Linear Algebra in agda   Guillermo Calderon
• [Agda] problem with `abstract'   Sergei Meshveliani
• [Agda] problem with `abstract'   Andreas Abel
• [Agda] problem with `abstract'   Sergei Meshveliani
• [Agda] problem with `abstract'   Sergei Meshveliani
• [Agda] problem with `abstract'   Andreas Abel
• parse error ? with open in telescope [Re: [Agda] problem with `abstract']   Andreas Abel
• parse error ? with open in telescope [Re: [Agda] problem with `abstract']   Sergei Meshveliani
• [Agda] problem with `abstract'   Sergei Meshveliani
• parse error ? with open in telescope [Re: [Agda] problem with `abstract']   Andreas Abel
• [Agda] problem with `abstract'   Andreas Abel
• parse error ? with open in telescope [Re: [Agda] problem with `abstract']   Sergei Meshveliani
• parse error ? with open in telescope [Re: [Agda] problem with `abstract']   Andreas Abel
• parse error ? with open in telescope [Re: [Agda] problem with `abstract']   mechvel at scico.botik.ru
• [Agda] Call for Participation: ICFP 2016   Lindsey Kuper
• [Agda] Call for Participation: ICFP 2016   Manuel Bärenz
• [Agda] Why does Agda think this is not strictly positive?   Roman
• [Agda] Why does Agda think this is not strictly positive?   Fredrik Nordvall Forsberg
• [Agda] Why does Agda think this is not strictly positive?   Frédéric Blanqui
• [Agda] Why does Agda think this is not strictly positive?   Roman
• [Agda] Why does Agda think this is not strictly positive?   Fredrik Nordvall Forsberg
• [Agda] Why does Agda think this is not strictly positive?   Roman
• [Agda] Why does Agda think this is not strictly positive?   Andreas Abel
• [Agda] Why does Agda think this is not strictly positive?   Roman
• [Agda] instance candidates in record fields   Guillermo Calderon
• [Agda] How to show a Term?   Roman
• [Agda] instance candidates in record fields   Andreas Abel
• [Agda] instance candidates in record fields   Andreas Abel
• [Agda] Call for Participation: WFLP 2016 and co-located events   Janis Voigtlaender
• [Agda] How to show a Term?   Ulf Norell
• [Agda] PEPM 2017 Second Call for Papers   Jeremy Yallop
• [Agda] How to show a Term?   Roman
• [Agda] How to show a Term?   Ulf Norell
• [Agda] on 2.5.2   Sergei Meshveliani
• [Agda] CPP 2017 Call for papers   bove at chalmers.se
• [Agda] PhD position in computational music structure analysis using functional programming   Wouter Swierstra
• [Agda] Postdoctoral position in programming languages at U Tuebingen   Klaus Ostermann
• [Agda] list for termination counter   Sergei Meshveliani
• [Agda] list for termination counter   G. Allais
• [Agda] list for termination counter   Sergei Meshveliani
• [Agda] Agda formalization of Dijkstra's algorithm?   Kenichi Asai
• [Agda] question on `with'   Sergei Meshveliani
• [Agda] question on `with'   Wolfram Kahl
• [Agda] question on `with'   Roman
• [Agda] question on `with'   Sergei Meshveliani
• [Agda] question on `with'   Ulf Norell
• [Agda] question on `with'   Sergei Meshveliani
• [Agda] question on `with'   Sergei Meshveliani
• [Agda] Using coinductive record constructor fails termination checking (2.5.1.1)   Sebastian Seufert
• [Agda] Using coinductive record constructor fails termination checking (2.5.1.1)   Andreas Abel
• [Agda] New edition of "Programming in Haskell"   Graham Hutton
• [Agda] help avoiding space leak using strict evaluation   Martin Stone Davis
• [Agda] PEPM 2017 Final Call for Papers (submission deadline extension: 30th Sep.)   Jeremy Yallop
• [Agda] help avoiding space leak using strict evaluation   Ulf Norell
• [Agda] help avoiding space leak using strict evaluation   Sergei Meshveliani
• [Agda] help avoiding space leak using strict evaluation   Ulf Norell
• [Agda] Record scoping issue   Jorn van Wijk
• [Agda] strictness application not unifying in the typechecker   Martin Stone Davis
• [Agda] strictness application not unifying in the typechecker   Ulf Norell
• [Agda] Record scoping issue   Nils Anders Danielsson
• [Agda] Record scoping issue   Roman
• [Agda] documentation for ".."   Martin Stone Davis
• [Agda] documentation for ".."   Ulf Norell
• [Agda] AIM XXIV - Utrecht, October 10 - 14   Wouter Swierstra
• [Agda] variables not bound with REWRITE pragma   Simon Boulier
• [Agda] variables not bound with REWRITE pragma   Jesper Cockx
• [Agda] variables not bound with REWRITE pragma   Jesper Cockx
• [Agda] variables not bound with REWRITE pragma   Simon Boulier
• [Agda] implicit lambda in Development Sep.16   Sergei Meshveliani
• [Agda] implicit lambda in Development Sep.16   Ulf Norell
• [Agda] implicit lambda in Development Sep.16   Sergei Meshveliani
• [Agda] dotted pattern for pair   Sergei Meshveliani
• [Agda] dotted pattern for pair   Andreas Abel
• [Agda] dotted pattern for pair   Ulf Norell
• [Agda] CFP, deadline Oct. 5: The 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP'17)   Yves Bertot
• [Agda] result code performance   Sergei Meshveliani
• [Agda] result code performance   Ulf Norell
• [Agda] result code performance   Sergei Meshveliani
• [Agda] result code performance   Ulf Norell
• [Agda] Private anonymous modules   Favonia
• [Agda] Nat arithmetic properties   Sergei Meshveliani
• [Agda] read-output Nat example   Sergei Meshveliani
• [Agda] Nat arithmetic properties   Ulf Norell
• [Agda] Nat arithmetic properties   Sergei Meshveliani
• [Agda] Nat arithmetic properties   Ulf Norell
• [Agda] read-output Nat example   Nils Anders Danielsson
• [Agda] Nat arithmetic properties   Sergei Meshveliani
• [Agda] Nat arithmetic properties   Ulf Norell
• [Agda] Nat arithmetic properties   Sergei Meshveliani
• [Agda] read-output Nat example   Sergei Meshveliani
• [Agda] file for readFiniteFile   Sergei Meshveliani
• [Agda] file for readFiniteFile   Nils Anders Danielsson
• [Agda] file for readFiniteFile   Sergei Meshveliani
• [Agda] file for readFiniteFile   Nils Anders Danielsson
• [Agda] file for readFiniteFile   G. Allais
• [Agda] file for readFiniteFile   Sergei Meshveliani
• [Agda] file for readFiniteFile   Nils Anders Danielsson
• [Agda] Nat arithmetic properties   Wolfram Kahl
• [Agda] Nat arithmetic properties   Sergei Meshveliani
• [Agda] file for readFiniteFile   Wolfram Kahl
• [Agda] Nat arithmetic properties   Roman
• [Agda] Nat arithmetic properties   Sergei Meshveliani
• [Agda] Nat arithmetic properties   Sergei Meshveliani
• [Agda] Nat arithmetic properties   Ulf Norell
• [Agda] Nat arithmetic properties   Ulf Norell
• [Agda] Nat arithmetic properties   Nils Anders Danielsson
• [Agda] Nat arithmetic properties   Sergei Meshveliani
• [Agda] Nat arithmetic properties   Ulf Norell
• [Agda] Nat arithmetic properties   Ulf Norell
• [Agda] Nat arithmetic properties   Sergei Meshveliani
• [Agda] Nat arithmetic performance   Sergei Meshveliani
• [Agda] Nat arithmetic performance   Ulf Norell
• [Agda] Nat arithmetic performance   Ulf Norell
• [Agda] There is probably no option to turn off postfix-projections   stvienna wiener
• [Agda] Nat arithmetic performance   Sergei Meshveliani
• [Agda] Nat arithmetic properties   Sergei Meshveliani
• [Agda] Nat arithmetic properties   Roman
• [Agda] There is probably no option to turn off postfix-projections   Andreas Abel
• [Agda] Implicit arguments inference   Valery Isaev
• [Agda] Implicit arguments inference   Roman
• [Agda] Implicit arguments inference   Valery Isaev
• [Agda] Implicit arguments inference   Ulf Norell
• [Agda] Final Call: CfP: RST@SAC 2017 - Marrakech, Morocco - April 3-7, 2016 (Deadline extended)   Faruk Caglar
• [Agda] no-eta-equality   Sergei Meshveliani
• [Agda] no-eta-equality   Andrea Vezzosi
• [Agda] no-eta-equality   Andrea Vezzosi
• [Agda] no-eta-equality   Sergei Meshveliani
• [Agda] no-eta-equality   Andrea Vezzosi
• [Agda] no-eta-equality   Sergei Meshveliani
• [Agda] no-eta-equality   Nils Anders Danielsson
• [Agda] no-eta-equality   Andrea Vezzosi
• [Agda] Agsy vs Unifier   Guido Martínez
• [Agda] Agsy vs Unifier   Andreas Abel
• [Agda] Agsy vs Unifier   Guido Martínez
• [Agda] Reflection: blockOnMeta after commitTC can cause a type error   Martin Stone Davis
• [Agda] no-eta-equality   Sergei Meshveliani
• [Agda] no-eta-equality   Andrea Vezzosi
• [Agda] no-eta-equality   Nils Anders Danielsson
• [Agda] no-eta-equality   Andrea Vezzosi
• [Agda] no-eta-equality   Sergei Meshveliani
• [Agda] no-eta-equality   Jesper Cockx
• [Agda] no-eta-equality   Ulf Norell
• [Agda] no-eta-equality   Wolfram Kahl
• [Agda] no-eta-equality   Ulf Norell
• [Agda] no-eta-equality   Nils Anders Danielsson
• [Agda] shared record parts   Sergei Meshveliani
• [Agda] second call: postdoc, research scientist, visiting student positions   Aaron Stump
• [Agda] re-checking   Sergei Meshveliani
• [Agda] evaluation strategy (was: shared record parts)   Martin Stone Davis
• [Agda] re-checking   Nils Anders Danielsson
• [Agda] example with --sharing   Sergei Meshveliani
• [Agda] example with --sharing   Ulf Norell
• [Agda] example with --sharing   Nils Anders Danielsson
• [Agda] re-checking   Sergei Meshveliani
• [Agda] LICS 2017 - CFP   Sam Staton
• [Agda] Internal error   Sergei Meshveliani
• [Agda] Math Research Communities on Homotopy Type Theory, June 4-10, 2017, Snowbird UT   Dan Licata
• [Agda] Internal error   Sergei Meshveliani
• [Agda] Journal of Functional Programming - Call for PhD Abstracts   Graham Hutton
• [Agda] Off the Beaten Track 2017: Call for Talk Proposals   Robert Atkey
• [Agda] add a "newbie questions" label to issue tracker?   Martin Stone Davis
• [Agda] add a "newbie questions" label to issue tracker?   Ulf Norell
• [Agda] add a "newbie questions" label to issue tracker?   Andreas Abel
• [Agda] reflection via FFI?   Martin Stone Davis
• [Agda] reflection via FFI?   Ulf Norell
• [Agda] reflection via FFI?   Roman
• [Agda] reflection via FFI?   Ulf Norell
• [Agda] reflection via FFI?   Roman
• [Agda] reflection via FFI?   Philipp Hausmann
• [Agda] reflection via FFI?   Ulf Norell
• [Agda] upgrading from 2.4.* to 2.5.1.1 (agda2-include-dirs problem)   Jacques Carette
• [Agda] upgrading from 2.4.* to 2.5.1.1 (agda2-include-dirs problem)   Nils Anders Danielsson
• [Agda] <Programming> 2017: Call for papers   Tim Molderez
• [Agda] ITP 2017 - First Call for Papers   Ana Bove
• [Agda] upgrading from 2.4.* to 2.5.1.1 (agda2-include-dirs problem)   Jacques Carette
• [Agda] upgrading from 2.4.* to 2.5.1.1 (agda2-include-dirs problem)   Nils Anders Danielsson
• [Agda] PEPM 2017 Call for Poster Papers (submission deadline Tuesday 8th November)   Jeremy Yallop
• [Agda] upgrading from 2.4.* to 2.5.1.1 (agda2-include-dirs problem)   Jacques Carette
• [Agda] upgrading from 2.4.* to 2.5.1.1 (agda2-include-dirs problem)   Nils Anders Danielsson
• [Agda] problems configuring haskell-mode and/or invoking cabal repl   Martin Stone Davis
• [Agda] evaluation strategies of the future [issue #426]   Martin Stone Davis
• [Agda] problems configuring haskell-mode and/or invoking cabal repl   Andreas Abel
• [Agda] evaluation strategies of the future [issue #426]   Ulf Norell
• [Agda] evaluation strategies of the future [issue #426]   Wolfram Kahl
• [Agda] evaluation strategies of the future [issue #426]   Ulf Norell
• [Agda] evaluation strategies of the future [issue #426]   Wolfram Kahl
• [Agda] evaluation strategies of the future [issue #426]   Ulf Norell
• [Agda] John C. Reynolds Doctoral Dissertation Award   Jeremy.Gibbons at cs.ox.ac.uk
• [Agda] evaluation strategies of the future [issue #426]   Sergei Meshveliani
• [Agda] evaluation strategies of the future [issue #426]   Ulf Norell
• [Agda] History of Agda   Ken Kubota
• [Agda] Re: History of Agda   Ulf Norell
• [Agda] Associativity of vector concatenation   Martin Escardo
• [Agda] Associativity of vector concatenation   Andrea Vezzosi
• [Agda] Associativity of vector concatenation   Tom Jack
• [Agda] Associativity of vector concatenation   Martin Escardo
• [Agda] Associativity of vector concatenation   Thorsten Altenkirch
• [Agda] Associativity of vector concatenation   Martin Escardo
• [Agda] Associativity of vector concatenation   Tom Jack
• [Agda] Associativity of vector concatenation   Roman
• [Agda] evaluation strategies of the future [issue #426]   Sergei Meshveliani
• [Agda] evaluation strategies of the future [issue #426]   Ulf Norell
• [Agda] evaluation strategies of the future [issue #426]   Sergei Meshveliani
• [Agda] Associativity of vector concatenation   Dan Licata
• [Agda] Associativity of vector concatenation   Martin Escardo
• [Agda] Associativity of vector concatenation   Dan Licata
• [Agda] Associativity of vector concatenation   Owen
• [Agda] Associativity of vector concatenation   Owen
• [Agda] Associativity of vector concatenation   Dan Licata
• [Agda] Associativity of vector concatenation   Owen
• [Agda] Call for Workshop Proposals: ICFP 2017   Lindsey Kuper
• [Agda] Cfa TTT 2017 (Type Theory Based Tools)   Andreas Abel
• [Agda] 'categories' library in 2.5.1.1   Jacques Carette
• [Agda] 'categories' library in 2.5.1.1   Andreas Abel
• [Agda] 'categories' library in 2.5.1.1   Jacques Carette
• [Agda] 'categories' library in 2.5.1.1   Miëtek Bak
• [Agda] Why is "strictly positive" more strict for record types?   Martin Stone Davis
• [Agda] Why is "strictly positive" more strict for record types?   Roman
• [Agda] Why is "strictly positive" more strict for record types?   Henning Basold
• [Agda] Re: 'categories' library in 2.5.1.1   Musa Al-hassy
• [Agda] Optimised equational reasoning   Nils Anders Danielsson
• [Agda] Optimised equational reasoning   Jacques Carette
• [Agda] Optimised equational reasoning   Nils Anders Danielsson
• [Agda] Optimised equational reasoning   Jacques Carette
• [Agda] Optimised equational reasoning   Andrew Pitts
• [Agda] Optimised equational reasoning   Andreas Abel
• [Agda] newbie instance resolution question: too many candidates?   Martin Stone Davis
• [Agda] newbie instance resolution question: too many candidates?   Ulf Norell
• [Agda] newbie instance resolution question: too many candidates?   Jesper Cockx
• [Agda] newbie instance resolution question: too many candidates?   Andreas Abel
• [Agda] newbie instance resolution question: too many candidates?   Jesper Cockx
• [Agda] newbie instance resolution question: too many candidates?   Andreas Abel
• [Agda] Macro not resolving implicit arguments as wished   João Paulo Pizani Flor
• [Agda] Ill-typed with construction   Jacques Carette
• [Agda] Using 'let' to pattern-match on single-constructor datatypes   Martin Stone Davis
• [Agda] Polymorphic Unit type with FFI / IO   stvienna wiener
• [Agda] Polymorphic Unit type with FFI / IO   G. Allais
• [Agda] Polymorphic Unit type with FFI / IO   Ulf Norell
• [Agda] Ill-typed with construction   Ulf Norell
• [Agda] Using 'let' to pattern-match on single-constructor datatypes   Andreas Abel
• [Agda] Macro not resolving implicit arguments as wished   Ulf Norell
• [Agda] Ill-typed with construction   Jacques Carette
• [Agda] 2nd Call for papers - <Programming> 2017   Tim Molderez
• [Agda] Off the Beaten Track 2017: Final Call for Talk Proposals; deadline extended   Robert Atkey
• [Agda] hints on switching between Agda versions   Andrew Pitts
• [Agda] hints on switching between Agda versions   Martin Escardo
• [Agda] hints on switching between Agda versions   Jesper Cockx
• [Agda] hints on switching between Agda versions   Manuel Bärenz
• [Agda] hints on switching between Agda versions   Ulf Norell
• [Agda] hints on switching between Agda versions   Adam Sandberg Eriksson
• [Agda] hints on switching between Agda versions   Andrew Pitts
• [Agda] hints on switching between Agda versions   Andrew Pitts
• [Agda] hints on switching between Agda versions   Martin Escardo
• [Agda] hints on switching between Agda versions   Andrew Pitts
• [Agda] hints on switching between Agda versions   Martin Escardo
• [Agda] hints on switching between Agda versions   Nils Anders Danielsson
• [Agda] hints on switching between Agda versions   Nils Anders Danielsson
• [Agda] Questions about unification   András Kovács
• [Agda] 2nd Cfa TTT 2017 (Type Theory Based Tools)   Andreas Abel
• [Agda] Questions about unification   Ulf Norell
• [Agda] Questions about unification   Roman
• [Agda] Questions about unification   András Kovács
• [Agda] Questions about unification   András Kovács
• [Agda] Questions about unification   Andreas Abel
• [Agda] Questions about unification   Roman
• [Agda] Questions about unification   András Kovács
• [Agda] Questions about unification   Andreas Abel
• [Agda] PhD studentships at FP lab, Nottingham   Thorsten Altenkirch
• [Agda] WiL 2017: Women in Logic Workshop Call for Papers   Amy Felty
• [Agda] installing 2.5.1.2   Sergei Meshveliani
• [Agda] installing 2.5.1.2   Andrés Sicard-Ramírez
• [Agda] installing 2.5.1.2   Sergei Meshveliani
• [Agda] installing 2.5.1.2   Andrés Sicard-Ramírez
• [Agda] stable version   Sergei Meshveliani
• [Agda] stable version   Ulf Norell
• [Agda] stable version   Sergei Meshveliani
• [Agda] stable version   Ulf Norell
• [Agda] how to reference to a version   Sergei Meshveliani
• [Agda] how to reference to a version   Andrés Sicard-Ramírez
• [Agda] how to reference to a version   Sergei Meshveliani
• [Agda] how to reference to a version   Andrés Sicard-Ramírez
• [Agda] how to reference to a version   Sergei Meshveliani
• [Agda] how to reference to a version   Andrés Sicard-Ramírez
• [Agda] how to reference to a version   Sergei Meshveliani
• [Agda] how to reference to a version   Ulf Norell
• [Agda] how to reference to a version   Sergei Meshveliani
• [Agda] how to reference to a version   Sergei Meshveliani
• [Agda] how to reference to a version   Ulf Norell
• [Agda] how to reference to a version   Sergei Meshveliani
• [Agda] how to reference to a version   Ulf Norell
• [Agda] repeated compilation   Sergei Meshveliani
• [Agda] repeated compilation   Andreas Abel
• [Agda] repeated compilation   Philipp Hausmann
• [Agda] repeated compilation   Ulf Norell
• [Agda] DoCon-A-0.04 announcement   Sergei Meshveliani
• [Agda] Partial Evaluation & Program Manipulation (PEPM'17): Call for Participation   Jeremy Yallop
• [Agda] This works in Idris by not in agda. (updating the type from the values of the constructor)   Apostolis Xekoukoulotakis
• [Agda] This works in Idris by not in agda. (updating the type from the values of the constructor)   Roman
• [Agda] This works in Idris by not in agda. (updating the type from the values of the constructor)   Jesper Cockx
• [Agda] This works in Idris by not in agda. (updating the type from the values of the constructor)   Andreas Abel
• [Agda] PhD positions on the AI4REASON project in Prague   Josef Urban
• [Agda] This works in Idris by not in agda. (updating the type from the values of the constructor)   Apostolis Xekoukoulotakis
• [Agda] Off the Beaten Track 2017: Call for Participation   Robert Atkey
• [Agda] [ANNOUNCE] Agda 2.5.2 release candidate 1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.2 release candidate 1   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.2   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Standard library 0.13   Andrés Sicard-Ramírez
• [Agda] Call for Papers: ICFP 2017   Lindsey Kuper
• [Agda] application announcement   Sergei Meshveliani
• [Agda] 'finitely supported' constructively and without decidable equality   Jacques Carette

Last message date: Fri Dec 30 16:02:40 CET 2016
Archived on: Fri Dec 30 16:02:44 CET 2016

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