2017 Archives by author

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

Starting: Wed Jan 4 21:58:07 CET 2017
Ending: Sun Dec 31 17:07:28 CET 2017
Messages: 734

• [Agda] Printing strings in the emacs mode   Setzer A.G.
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Andreas Abel
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Andreas Abel
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Andreas Abel
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Andreas Abel
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Andreas Abel
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Andreas Abel
• [Agda] type check performance   Andreas Abel
• [Agda] hidden agda options / getting more info about unsolved metas   Andreas Abel
• [Agda] Levels and Containers   Andreas Abel
• [Agda] Removing a deducible Size constrain leads to error.   Andreas Abel
• [Agda] [Coq-Club] ESSLLI student session CFP: Deadline extended until Feb 14   Andreas Abel
• [Agda] text-icu-0.7.0.1   Andreas Abel
• [Agda] How safe is Type:Type?   Andreas Abel
• [Agda] How safe is Type:Type?   Andreas Abel
• [Agda] How safe is Type:Type?   Andreas Abel
• [Agda] Maintain compatibility with ghc 7.8?   Andreas Abel
• [Agda] Maintain compatibility with ghc 7.8?   Andreas Abel
• [Agda] Trouble with sizes   Andreas Abel
• [Agda] Many ways to open a module - Is there a reason?   Andreas Abel
• [Agda] pattern matching order   Andreas Abel
• [Agda] pattern matching order   Andreas Abel
• [Agda] pattern matching order   Andreas Abel
• [Agda] pattern matching order   Andreas Abel
• [Agda] Case split creates too many {_}   Andreas Abel
• [Agda] Printing named arguments [Re: Case split creates too many {_}]   Andreas Abel
• [Agda] When to use implicit arguments [Re: Printing named arguments]   Andreas Abel
• [Agda] Typing.CheckRHS   Andreas Abel
• [Agda] ⊓ in Nat   Andreas Abel
• [Agda] Senior Lectureships in Computer Science at Chalmers and Gothenburg U   Andreas Abel
• [Agda] Problems with strict positivity   Andreas Abel
• [Agda] `search' format   Andreas Abel
• [Agda] APLAS 2017 call for papers   Andreas Abel
• [Agda] Should adding eta-equality help here?   Andreas Abel
• [Agda] possible unifier bug / explain error messages?   Andreas Abel
• [Agda] strange mismatch   Andreas Abel
• [Agda] constructor injectiveness   Andreas Abel
• [Agda] termination with `where'   Andreas Abel
• [Agda] APLAS 2017: June 13 deadline, 2nd CfP, Asian Symposium on Programming Languages and Systems   Andreas Abel
• [Agda] 1-infix-2   Andreas Abel
• [Agda] matching against _::_ ?   Andreas Abel
• [Agda] Caching [Re: Type checking times and a solution.]   Andreas Abel
• [Agda] Caching [Re: Type checking times and a solution.]   Andreas Abel
• [Agda] matching against _::_ ?   Andreas Abel
• [Agda] matching against _::_ ?   Andreas Abel
• [Agda] Proposed notation for universe polymorphism   Andreas Abel
• [Agda] parameters vs indices   Andreas Abel
• [Agda] missing import overlap   Andreas Abel
• [Agda] StrictLex in library   Andreas Abel
• [Agda] Why does unification work here?   Andreas Abel
• [Agda] Why does unification work here?   Andreas Abel
• [Agda] Some problems with K-S basis   Andreas Abel
• [Agda] Irrelevance and resurrection in type signatures   Andreas Abel
• [Agda] Bezonas helpon !   Andreas Abel
• [Agda] Bezonas helpon !   Andreas Abel
• [Agda] Bezonas helpon !   Andreas Abel
• [Agda] Bezonas helpon !   Andreas Abel
• [Agda] [ANNOUNCE] Agda 2.5.3   Andreas Abel
• [Agda] [ANNOUNCE] Agda 2.5.3   Andreas Abel
• [Agda] [ANNOUNCE] Agda 2.5.3   Andreas Abel
• [Agda] No Agda AIM meeting any more?   Andreas Abel
• [Agda] Use the ring solver with an abstract ring   Andreas Abel
• [Agda] Fwd: [FP] FW: Google Internships in Programming Languages, Compilers, and Software Engineering (2018)   Andreas Abel
• [Agda] [REQUEST] Help with transition from 2.5.1/2 (std-lib 0.12) to 2.5.3 (std-lib 0.14)   Andreas Abel
• [Agda] instance arguments and negation.   Andreas Abel
• [Agda] Agda's syntax declaration   Andreas Abel
• [Agda] Printing strings in the emacs mode   Andreas Abel
• [Agda] dotted patterns   Andreas Abel
• [Agda] Universe level checking   Andreas Abel
• [Agda] Trying to load modules from Norell OPLSS tutorial   Andreas Abel
• [Agda] Non-termination help!   Andreas Abel
• [Agda] Non-termination help!   Andreas Abel
• [Agda] How to get rid of warning   Andreas Abel
• [Agda] How to get rid of warning   Andreas Abel
• [Agda] Disappearing unicode in Literate Agda - XeLatex   Andreas Abel
• [Agda] 1st call for papers: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury   Peter Achten
• [Agda] 2nd call for papers: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury   Peter Achten
• [Agda] Final call for papers: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury   Peter Achten
• [Agda] Deadline extension may 15: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury   Peter Achten
• [Agda] Call for participation: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury   Peter Achten
• [Agda] Call for participation: Trends in Functional Programming, 19-21 june 2017 AND Trends in Functional Programming in Education, 22 june 2017, University of Kent, Canterbury   Peter Achten
• [Agda] Oregon PL Summer School 2017: call for participation   Amal Ahmed
• [Agda] Oregon PL Summer School 2017: register by April 1   Amal Ahmed
• [Agda] OPLSS: register by April 15th   Amal Ahmed
• [Agda] Call for Contributions: Foundations for Practical Formalization of Mathematics   Benedikt Ahrens
• [Agda] type check performance   G. Allais
• [Agda] example with insertion to list   G. Allais
• [Agda] example with insertion to list   G. Allais
• [Agda] proof for insertion to a list   G. Allais
• [Agda] FOREIGN GHC pragma triggers parse error   G. Allais
• [Agda] Fix emacs compile hook after updating to new agda version   G. Allais
• [Agda] Maintain compatibility with ghc 7.8?   G. Allais
• [Agda] Some problems with K-S basis   G. Allais
• [Agda] email list reference   G. Allais
• [Agda] email list reference   G. Allais
• [Agda] email list reference   G. Allais
• [Agda] installing/using 2.6.0-207bde6   G. Allais
• [Agda] common super-structure   Guillaume Allais
• [Agda] Agda code in slides   Guillaume Allais
• [Agda] Non-termination help!   Guillaume Allais
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Thorsten Altenkirch
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Thorsten Altenkirch
• [Agda] type check performance   Thorsten Altenkirch
• [Agda] 'finitely supported' constructively and without decidable equality   Thorsten Altenkirch
• [Agda] Propositional equality for coinductive records   Thorsten Altenkirch
• [Agda] pattern matching order   Thorsten Altenkirch
• [Agda] pattern matching order   Thorsten Altenkirch
• [Agda] parameters vs indices   Thorsten Altenkirch
• [Agda] parameters vs indices   Thorsten Altenkirch
• [Agda] parameters vs indices   Thorsten Altenkirch
• [Agda] parameters vs indices   Thorsten Altenkirch
• [Agda] PhD positions at Nottingham   Thorsten Altenkirch
• [Agda] Call for Contributions: Workshop on HoTT/UF (with FSCD 2017)   Anders
• [Agda] [ANNOUNCE] Agda 2.5.2   Kenichi Asai
• [Agda] Agda installation for all users   Kenichi Asai
• [Agda] The University of Strathclyde’s Global Talent Programme - Security and Data Sciences   Robert Atkey
• [Agda] Interactive Theorem Proving (ITP) 2018: Second CFP   Jeremy Avigad
• [Agda] Call for bids to host ITP 2019   Jeremy Avigad
• [Agda] Naive person's questions about agda vs. haskell symbol notation   Miëtek Bak
• [Agda] parameters vs indices   Henning Basold
• [Agda] parameters vs indices   Henning Basold
• [Agda] parameters vs indices   Henning Basold
• [Agda] CMCS 2018: Second Call for Papers   Henning Basold
• [Agda] CMCS 2018: Final Call for Papers   Henning Basold
• [Agda] Two PhD positions in Ljubljana starting October 2017   Andrej Bauer
• [Agda] PhD offer on Integrating automated provers in proof assistants   Frédéric Blanqui
• [Agda] LFMTP'18 Call for Papers   Ana Bove
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Jan Bracker
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Jan Bracker
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Jan Bracker
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Jan Bracker
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Jan Bracker
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Jan Bracker
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Jan Bracker
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Jan Bracker
• [Agda] productivity of fibonacci stream   Guillaume Brunerie
• [Agda] Instance arguments vs auto in Idris.   Guillaume Brunerie
• [Agda] Instance arguments vs auto in Idris.   Guillaume Brunerie
• [Agda] Printing strings in the emacs mode   Guillaume Brunerie
• [Agda] Printing strings in the emacs mode   Guillaume Brunerie
• [Agda] Levels and Containers   Manuel Bärenz
• [Agda] Trouble with sizes   Manuel Bärenz
• [Agda] Problems with strict positivity   Manuel Bärenz
• [Agda] Problems with strict positivity   Manuel Bärenz
• [Agda] Some proofs by clauses   Manuel Bärenz
• [Agda] ⊥-elim and proof duplication. Is there another way?   Guillermo Calderon
• [Agda] How do I check whether an agda term associated with a specific name relies on hole?   Anthony Cantor
• [Agda] 'finitely supported' constructively and without decidable equality   Jacques Carette
• [Agda] 'finitely supported' constructively and without decidable equality   Jacques Carette
• [Agda] type check performance   Jacques Carette
• [Agda] AMMCS-2017 call for submissions   Jacques Carette
• [Agda] making a pair explodes   Jacques Carette
• [Agda] Standard library mailing list?   Jacques Carette
• [Agda] Request of suggestion of learning material for Agda   Mario Castelán Castro
• [Agda] Bezonas helpon !   Mario Castelán Castro
• [Agda] Request of suggestion of learning material for Agda   Mario Castelán Castro
• [Agda] Request of suggestion of learning material for Agda   Mario Castelán Castro
• [Agda] Can intuitionistic type theory express derivations of physical equations more strictly?   Mario Castelán Castro
• [Agda] 1st CfP: SLE 2017 (10th ACM SIGPLAN International Conference on Software Language Engineering)   Andrei Chis
• [Agda] 2nd CfP: SLE 2017 (10th ACM SIGPLAN International Conference on Software Language Engineering)   Andrei Chis
• [Agda] 3rd CfP: SLE 2017 (10th ACM SIGPLAN International Conference on Software Language Engineering)   Andrei Chis
• [Agda] Deadline Extension - SLE 2017 (10th ACM SIGPLAN International Conference on Software Language Engineering)   Andrei Chis
• [Agda] Adding "print" to TC monad?   David Christiansen
• [Agda] type check performance   Jesper Cockx
• [Agda] type check performance   Jesper Cockx
• [Agda] Sized types unification error.   Jesper Cockx
• [Agda] text-icu-0.7.0.1   Jesper Cockx
• [Agda] How safe is Type:Type?   Jesper Cockx
• [Agda] How safe is Type:Type?   Jesper Cockx
• [Agda] Agda options   Jesper Cockx
• [Agda] Help at propositional equality proof that contains subst.   Jesper Cockx
• [Agda] Help at propositional equality proof that contains subst.   Jesper Cockx
• [Agda] missed wildcard pattern   Jesper Cockx
• [Agda] missed wildcard pattern   Jesper Cockx
• [Agda] When catchall does not help.   Jesper Cockx
• [Agda] rewriting and parameterized modules   Jesper Cockx
• [Agda] rewriting and parameterized modules   Jesper Cockx
• [Agda] copyrights   Jesper Cockx
• [Agda] Bezonas helpon !   Jesper Cockx
• [Agda] Cannot apply injectivity   Jesper Cockx
• [Agda] Cannot apply injectivity   Jesper Cockx
• [Agda] dotted patterns   Jesper Cockx
• [Agda] [ANNOUNCE] Standard library 0.14   Matthew Daggitt
• [Agda] Disappearing unicode in Literate Agda - XeLatex   Matthew Daggitt
• [Agda] Disappearing unicode in Literate Agda - XeLatex   Matthew Daggitt
• [Agda] type check performance   Nils Anders Danielsson
• [Agda] 'finitely supported' constructively and without decidable equality   Nils Anders Danielsson
• [Agda] type check performance   Nils Anders Danielsson
• [Agda] Holes 0.1.0   Nils Anders Danielsson
• [Agda] Levels and Containers   Nils Anders Danielsson
• [Agda] `case' vs `with'   Nils Anders Danielsson
• [Agda] strictness switch   Nils Anders Danielsson
• [Agda] {} for nested `with' syntax   Nils Anders Danielsson
• [Agda] Agda installation for all users   Nils Anders Danielsson
• [Agda] signature for `with' branch   Nils Anders Danielsson
• [Agda] signature for `with' branch   Nils Anders Danielsson
• [Agda] signature for `with' branch   Nils Anders Danielsson
• [Agda] Fix emacs compile hook after updating to new agda version   Nils Anders Danielsson
• [Agda] Agda options   Nils Anders Danielsson
• [Agda] infix ∸-mono ?   Nils Anders Danielsson
• [Agda] infix ∸-mono ?   Nils Anders Danielsson
• [Agda] possible unifier bug / explain error messages?   Nils Anders Danielsson
• [Agda] Standard library mailing list?   Nils Anders Danielsson
• [Agda] When catchall does not help.   Nils Anders Danielsson
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Nils Anders Danielsson
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Nils Anders Danielsson
• [Agda] unstable composition checking   Nils Anders Danielsson
• [Agda] summing rationals   Nils Anders Danielsson
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Nils Anders Danielsson
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Nils Anders Danielsson
• [Agda] Instance fields   Nils Anders Danielsson
• [Agda] guidelines for reporting internal errors   Nils Anders Danielsson
• [Agda] type check cost   Nils Anders Danielsson
• [Agda] on standard library   Nils Anders Danielsson
• [Agda] Agda code in slides   Nils Anders Danielsson
• [Agda] `with' in standard functions   Nils Anders Danielsson
• [Agda] `with' in standard functions   Nils Anders Danielsson
• [Agda] `with' in standard functions   Nils Anders Danielsson
• [Agda] Agda's syntax declaration   Nils Anders Danielsson
• [Agda] Installing libraries   Nils Anders Danielsson
• [Agda] difficult termination   Nils Anders Danielsson
• [Agda] `<' reasoning   Nils Anders Danielsson
• [Agda] numeric literals   Nils Anders Danielsson
• [Agda] How to get rid of warning   Nils Anders Danielsson
• [Agda] How to get rid of warning   Nils Anders Danielsson
• [Agda] Disappearing unicode in Literate Agda - XeLatex   Nils Anders Danielsson
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Martin Stone Davis
• [Agda] hidden agda options / getting more info about unsolved metas   Martin Stone Davis
• [Agda] hidden agda options / getting more info about unsolved metas   Martin Stone Davis
• [Agda] pattern for All is not matched   Martin Stone Davis
• [Agda] pattern for All is not matched   Martin Stone Davis
• [Agda] strange let-in-case-let   Martin Stone Davis
• [Agda] strange let-in-case-let   Martin Stone Davis
• [Agda] help explaining instance resolution   Martin Stone Davis
• [Agda] help explaining instance resolution   Martin Stone Davis
• [Agda] help explaining instance resolution   Martin Stone Davis
• [Agda] Should adding eta-equality help here?   Martin Stone Davis
• [Agda] possible unifier bug / explain error messages?   Martin Stone Davis
• [Agda] Instance fields   Martin Stone Davis
• [Agda] Instance fields   Martin Stone Davis
• [Agda] guidelines for reporting internal errors   Martin Stone Davis
• [Agda] Instance fields   Martin Stone Davis
• [Agda] discovering verbosity options   Martin Stone Davis
• [Agda] failure to solve b/c undecidable? custom meta solvers?   Martin Stone Davis
• [Agda] problems installing agda master using stack   Martin Stone Davis
• [Agda] Fwd: Re: problems installing agda master using stack   Martin Stone Davis
• [Agda] Multiple Research Positions, ERC MATHADOR Project, IMDEA Software Institute, Madrid, Spain   Germán Andrés Delbianco
• [Agda] Call for Presentations on Secure Compilation (PriSC Workshop @ POPL'18)   Dominique Devriese
• [Agda] Final call for Secure Compilation presentations (PriSC Workshop @ POPL'18)   Dominique Devriese
• [Agda] PriSC'18 deadline extended by 1 week   Dominique Devriese
• [Agda] Call for Participation for Secure Compilation Workshop (PriSC @ POPL'18)   Dominique Devriese
• [Agda] Call for Short Talks on Secure Compilation (PriSC Workshop @ POPL'18)   Dominique Devriese
• [Agda] How safe is Type:Type?   Martin Escardo
• [Agda] Date for PhD defense   Martin Escardo
• [Agda] Date for PhD defense   Martin Escardo
• [Agda] pattern matching order   Martin Escardo
• [Agda] pattern matching order   Martin Escardo
• [Agda] Help at propositional equality proof that contains subst.   Martin Escardo
• [Agda] Proposed notation for universe polymorphism   Martin Escardo
• [Agda] Request of suggestion of learning material for Agda   Martin Escardo
• [Agda] School and workshop on univalent mathematics, 11-15 Dec, Birmingham (UK)   Martin Escardo
• [Agda] Can intuitionistic type theory express derivations of physical equations more strictly?   Martin Escardo
• [Agda] decidable equality in algebra   Martin Escardo
• [Agda] decidable equality in algebra   Martin Escardo
• [Agda] Agda's syntax declaration   Martin Escardo
• [Agda] Agda's syntax declaration   Martin Escardo
• [Agda] Agda's syntax declaration   Martin Escardo
• [Agda] Agda's syntax declaration   Martin Escardo
• [Agda] Agda's syntax declaration   Martin Escardo
• [Agda] difficult termination   Martin Escardo
• [Agda] Universe level checking   Martin Escardo
• [Agda] How to get rid of warning   Martin Escardo
• [Agda] Font questions again   Martin Escardo
• [Agda] Proposed notation for universe polymorphism   Martín Hötzel Escardó
• [Agda] dotted patterns   Martín Hötzel Escardó
• [Agda] Universe level checking   Martín Hötzel Escardó
• [Agda] Universe level checking   Martín Hötzel Escardó
• [Agda] How to get rid of warning   Martín Hötzel Escardó
• [Agda] How to get rid of warning   Martín Hötzel Escardó
• [Agda] WiL 2017: Women in Logic Workshop Second Call for Papers (new dates)   Amy Felty
• [Agda] the Racket summer school of semantics and languages   Robby Findler
• [Agda] 'finitely supported' constructively and without decidable equality   Fredrik Nordvall Forsberg
• [Agda] [ANNOUNCE] Agda 2.5.2   Oleg Grenrus
• [Agda] <Programming> 2018: 2nd Call for Papers   Sylvia Grewe
• [Agda] CfP <Programming> 2018: Research Papers Third Submission Deadline   Sylvia Grewe
• [Agda] <Programming> 2018: Call for workshop, symposium & poster submissions   Sylvia Grewe
• [Agda] type check performance   Peter Hancock
• [Agda] Naive person's questions about agda vs. haskell symbol notation   Peter Hancock
• [Agda] Holes 0.1.0   Bradley Hardy
• [Agda] Holes 0.1.0   Bradley Hardy
• [Agda] Call for Participation: Workshop on HoTT/UF (with FSCD 2017)   Simon Huber
• [Agda] Journal of Functional Programming - Call for PhD Abstracts   Graham Hutton
• [Agda] CALL FOR PAPERS - GraMSec 2017   Harley D. Eades III
• [Agda] Request of suggestion of learning material for Agda   Harley D. Eades III
• [Agda] Can intuitionistic type theory express derivations of physical equations more strictly?   Hidekazu IWAKI
• [Agda] Can intuitionistic type theory express derivations of physical equations more strictly?   Hidekazu IWAKI
• [Agda] Fwd: Can intuitionistic type theory express derivations of physical equations more strictly?   Hidekazu IWAKI
• [Agda] Agda's syntax declaration   Frederik Hanghøj Iversen
• [Agda] Agda's syntax declaration   Frederik Hanghøj Iversen
• [Agda] Installing libraries   Frederik Hanghøj Iversen
• [Agda] FYI: CFP CICM 2017   Patrik Jansson
• [Agda] AIM XXV - Gothenburg, May 9 - 15   Víctor López Juan
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Wolfram Kahl
• [Agda] type check performance   Wolfram Kahl
• [Agda] type check performance   Wolfram Kahl
• [Agda] signature for `with' branch   Wolfram Kahl
• [Agda] about serialization   Wolfram Kahl
• [Agda] Vezzosi's patch   Wolfram Kahl
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Wolfram Kahl
• [Agda] Agda's syntax declaration   Wolfram Kahl
• [Agda] TYPES 2017 call for contributions   Ambrus Kaposi
• [Agda] TYPES 2017 2nd call for contributions   Ambrus Kaposi
• [Agda] TYPES 2017 submission deadline extended   Ambrus Kaposi
• [Agda] Call for participation: TYPES 2017. Registration is open   Ambrus Kaposi
• [Agda] rewriting and parameterized modules   Ambrus Kaposi
• [Agda] TYPES 2017 post-proceedings open call for papers   Ambrus Kaposi
• [Agda] TYPES 2017 post-proceedings open call for papers   Ambrus Kaposi
• [Agda] TYPES 2017 post-proceedings call for papers   Ambrus Kaposi
• [Agda] TYPES 2017 post-proceedings DEADLINE EXTENDED   Ambrus Kaposi
• [Agda] AIM XXVI - Budapest, 29 Jan -- 3 Feb 2018   Ambrus Kaposi
• [Agda] Agda Implementors' Meeting XXVI - Budapest, 29 Jan -- 3 Feb 2018   Ambrus Kaposi
• [Agda] Call for Conference Grant Applications (Inclusiveness Target Countries)   Ambrus Kaposi
• [Agda] Use the ring solver with an abstract ring   Chantal Keller
• [Agda] Fully funded PhD position in CS at Heriot-Watt University, Edinburgh, Scotland   Ekaterina Komendantskaya
• [Agda] Why does unification work here?   András Kovács
• [Agda] Why does unification work here?   András Kovács
• [Agda] type check performance   Robbert Krebbers
• [Agda] type check performance   Neel Krishnaswami
• [Agda] productivity of fibonacci stream   Adam Krupicka
• [Agda] Second Call for Papers: ICFP 2017   Lindsey Kuper
• [Agda] Final Call for Papers: ICFP 2017   Lindsey Kuper
• [Agda] Call for Participation: ICFP 2017   Lindsey Kuper
• [Agda] Call for Participation: ICFP 2017   Lindsey Kuper
• [Agda] Call for Workshop Proposals: ICFP 2018   Lindsey Kuper
• [Agda] Call for Sponsorships: ICFP 2018   Lindsey Kuper
• [Agda] Call for Papers: PACMPL issue ICFP 2018   Lindsey Kuper
• [Agda] 'finitely supported' constructively and without decidable equality   Twan van Laarhoven
• [Agda] type check performance   Larrytheliquid
• [Agda] Bezonas helpon !   Serge Leblanc
• [Agda] Bezonas helpon !   Serge Leblanc
• [Agda] Bezonas helpon !   Serge Leblanc
• [Agda] Bezonas helpon !   Serge Leblanc
• [Agda] Bezonas helpon !   Serge Leblanc
• [Agda] Bezonas helpon !   Serge Leblanc
• [Agda] Bezonas helpon !   Serge Leblanc
• [Agda] Bezonas helpon !   Serge Leblanc
• [Agda] Bezonas helpon !   Serge Leblanc
• [Agda] Request of suggestion of learning material for Agda   John Leo
• [Agda] Font questions again   John Leo
• [Agda] Workshop on Termination and Circular Proofs (Chambéry, 19/07)   Rodolphe Lepigre
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Dan Licata
• [Agda] Math Research Communities on Homotopy Type Theory, June 4-10, 2017, Snowbird UT   Dan Licata
• [Agda] Propositional equality for coinductive records   Jannis Limperg
• [Agda] Propositional equality for coinductive records   Jannis Limperg
• [Agda] _<_ of agda-prelude   Jannis Limperg
• [Agda] how do I handle absurd with patterns?   Jannis Limperg
• [Agda] Fixpoint in Agda   Jannis Limperg
• [Agda] Non-termination help!   Martín
• [Agda] Non-termination help!   Martín
• [Agda] Non-termination help!   Martín
• [Agda] strange mismatch   MONTIN Mathieu
• [Agda] [REQUEST] Help with transition from 2.5.1/2 (std-lib 0.12) to 2.5.3 (std-lib 0.14)   James McKinna
• [Agda] [REQUEST] Help with transition from 2.5.1/2 (std-lib 0.12) to 2.5.3 (std-lib 0.14)   James McKinna
• [Agda] type check performance   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] strictness switch   Sergei Meshveliani
• [Agda] pattern for All is not matched   Sergei Meshveliani
• [Agda] pattern for All is not matched   Sergei Meshveliani
• [Agda] strange let-in-case-let   Sergei Meshveliani
• [Agda] strange let-in-case-let   Sergei Meshveliani
• [Agda] strange let-in-case-let   Sergei Meshveliani
• [Agda] `case' vs `with'   Sergei Meshveliani
• [Agda] example with insertion to list   Sergei Meshveliani
• [Agda] example with insertion to list   Sergei Meshveliani
• [Agda] example with insertion to list   Sergei Meshveliani
• [Agda] example with insertion to list   Sergei Meshveliani
• [Agda] Failed to find source of module   Sergei Meshveliani
• [Agda] Failed to find source of module   Sergei Meshveliani
• [Agda] proof for insertion to a list   Sergei Meshveliani
• [Agda] proof for insertion to a list   Sergei Meshveliani
• [Agda] text-icu-0.7.0.1   Sergei Meshveliani
• [Agda] proof for insertion to a list   Sergei Meshveliani
• [Agda] {} for nested `with' syntax   Sergei Meshveliani
• [Agda] more about insertion to a list   Sergei Meshveliani
• [Agda] more about insertion to a list   Sergei Meshveliani
• [Agda] more about insertion to a list   Sergei Meshveliani
• [Agda] signature for `with' branch   Sergei Meshveliani
• [Agda] signature for `with' branch   Sergei Meshveliani
• [Agda] signature for `with' branch   Sergei Meshveliani
• [Agda] signature for `with' branch   Sergei Meshveliani
• [Agda] signature for `with' branch   Sergei Meshveliani
• [Agda] signature for `with' branch   Sergei Meshveliani
• [Agda] example with nested `with'   Sergei Meshveliani
• [Agda] Agda options   Sergei Meshveliani
• [Agda] about serialization   Sergei Meshveliani
• [Agda] about serialization   Sergei Meshveliani
• [Agda] about serialization   Sergei Meshveliani
• [Agda] about serialization   Sergei Meshveliani
• [Agda] about serialization   Sergei Meshveliani
• [Agda] about serialization   Sergei Meshveliani
• [Agda] Vezzosi's patch   Sergei Meshveliani
• [Agda] Vezzosi's patch   Sergei Meshveliani
• [Agda] making a pair explodes   Sergei Meshveliani
• [Agda] making a pair explodes   Sergei Meshveliani
• [Agda] making a pair explodes   Sergei Meshveliani
• [Agda] making a pair explodes   Sergei Meshveliani
• [Agda] Typing.CheckRHS   Sergei Meshveliani
• [Agda] old .agdai   Sergei Meshveliani
• [Agda] Typing.CheckRHS   Sergei Meshveliani
• [Agda] Typing.CheckRHS   Sergei Meshveliani
• [Agda] Typing.CheckRHS   Sergei Meshveliani
• [Agda] length-* in library   Sergei Meshveliani
• [Agda] ⊓ in Nat   Sergei Meshveliani
• [Agda] ⊓ in Nat   Sergei Meshveliani
• [Agda] `search' format   Sergei Meshveliani
• [Agda] `search' format   Sergei Meshveliani
• [Agda] infix ∸-mono ?   Sergei Meshveliani
• [Agda] Char + String   Sergei Meshveliani
• [Agda] Char + String   Sergei Meshveliani
• [Agda] Char + String   Sergei Meshveliani
• [Agda] notes on type check performance   Sergei Meshveliani
• [Agda] notes on type check performance   Sergei Meshveliani
• [Agda] strange mismatch   Sergei Meshveliani
• [Agda] strange mismatch   Sergei Meshveliani
• [Agda] strange mismatch   Sergei Meshveliani
• [Agda] strange mismatch   Sergei Meshveliani
• [Agda] constructor injectiveness   Sergei Meshveliani
• [Agda] missed wildcard pattern   Sergei Meshveliani
• [Agda] termination with `where'   Sergei Meshveliani
• [Agda] 1-infix-2   Sergei Meshveliani
• [Agda] 1-infix-2   Sergei Meshveliani
• [Agda] matching against _::_ ?   Sergei Meshveliani
• [Agda] matching against _::_ ?   Sergei Meshveliani
• [Agda] matching against _::_ ?   Sergei Meshveliani
• [Agda] matching against _::_ ?   Sergei Meshveliani
• [Agda] unstable composition checking   Sergei Meshveliani
• [Agda] is divMod slow?   Sergei Meshveliani
• [Agda] is divMod slow?   Sergei Meshveliani
• [Agda] is divMod slow?   Sergei Meshveliani
• [Agda] is divMod slow?   Sergei Meshveliani
• [Agda] timing for agda-prelude gcd   Sergei Meshveliani
• [Agda] timing for agda-prelude gcd   Sergei Meshveliani
• [Agda] _<_ of agda-prelude   Sergei Meshveliani
• [Agda] _<_ of agda-prelude   Sergei Meshveliani
• [Agda] summing rationals   Sergei Meshveliani
• [Agda] summing rationals   Sergei Meshveliani
• [Agda] summing rationals   Sergei Meshveliani
• [Agda] summing rationals   Sergei Meshveliani
• [Agda] swap in record ambiguity   Sergei Meshveliani
• [Agda] swap in record ambiguity   Sergei Meshveliani
• [Agda] missing import overlap   Sergei Meshveliani
• [Agda] unstable composition checking   Sergei Meshveliani
• [Agda] address in lib pull request   Sergei Meshveliani
• [Agda] address in lib pull request   Sergei Meshveliani
• [Agda] StrictLex in library   Sergei Meshveliani
• [Agda] StrictLex in library   Sergei Meshveliani
• [Agda] updating pull request   Sergei Meshveliani
• [Agda] Some problems with K-S basis   Sergei Meshveliani
• [Agda] divmod-unique of Agda prelude   Sergei Meshveliani
• [Agda] copyrights   Sergei Meshveliani
• [Agda] email list reference   Sergei Meshveliani
• [Agda] email list reference   Sergei Meshveliani
• [Agda] email list reference   Sergei Meshveliani
• [Agda] email list reference   Sergei Meshveliani
• [Agda] installing/using 2.6.0-207bde6   Sergei Meshveliani
• [Agda] installing/using 2.6.0-207bde6   Sergei Meshveliani
• [Agda] installing/using 2.6.0-207bde6   Sergei Meshveliani
• [Agda] Bezonas helpon !   Sergei Meshveliani
• [Agda] Bezonas helpon !   Sergei Meshveliani
• [Agda] Bezonas helpon !   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.3 release candidate 1   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.3 release candidate 1   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.3 release candidate 1   Sergei Meshveliani
• [Agda] type check cost   Sergei Meshveliani
• [Agda] type check cost   Sergei Meshveliani
• [Agda] type check cost   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.3   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.3   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.3   Sergei Meshveliani
• [Agda] [ANNOUNCE] Agda 2.5.3   Sergei Meshveliani
• [Agda] common super-structure   Sergei Meshveliani
• [Agda] DoCon-A-2.00 announce   Sergei Meshveliani
• [Agda] on standard library   Sergei Meshveliani
• [Agda] common super-structure   Sergei Meshveliani
• [Agda] Agda code in slides   Sergei Meshveliani
• [Agda] Agda code in slides   Sergei Meshveliani
• [Agda] `with' in standard functions   Sergei Meshveliani
• [Agda] `with' in standard functions   Sergei Meshveliani
• [Agda] `with' in standard functions   Sergei Meshveliani
• [Agda] `with' in standard functions   Sergei Meshveliani
• [Agda] `with' in standard functions   Sergei Meshveliani
• [Agda] `with' in standard functions   Sergei Meshveliani
• [Agda] decidable equality in algebra   Sergei Meshveliani
• [Agda] decidable equality in algebra   Sergei Meshveliani
• [Agda] difficult termination   Sergei Meshveliani
• [Agda] difficult termination   Sergei Meshveliani
• [Agda] difficult termination   Sergei Meshveliani
• [Agda] difficult termination   Sergei Meshveliani
• [Agda] on `data' declaration   Sergei Meshveliani
• [Agda] on `data' declaration   Sergei Meshveliani
• [Agda] `<' reasoning   Sergei Meshveliani
• [Agda] `<' reasoning   Sergei Meshveliani
• [Agda] Nat for termination counter   Sergei Meshveliani
• [Agda] original Nat   Sergei Meshveliani
• [Agda] original Nat   Sergei Meshveliani
• [Agda] original Nat   Sergei Meshveliani
• [Agda] numeric literals   Sergei Meshveliani
• [Agda] no-built-in version   Sergei Meshveliani
• [Agda] `let' in function signature   Sergei Meshveliani
• [Agda] `let' in function signature   Sergei Meshveliani
• [Agda] Holes 0.1.0   Victor Miraldo
• [Agda] Holes 0.1.0   Victor Miraldo
• [Agda] <Programming> 2017: Call for workshop, symposium & poster submissions   Tim Molderez
• [Agda] <Programming> 2017: Final call for workshop, symposium, demo & poster submissions   Tim Molderez
• [Agda] <Programming> 2017: Call for participation   Tim Molderez
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Stefan Monnier
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Stefan Monnier
• [Agda] type check performance   Stefan Monnier
• [Agda] How safe is Type:Type?   Stefan Monnier
• [Agda] How safe is Type:Type?   Stefan Monnier
• [Agda] Universe level checking   Stefan Monnier
• [Agda] 2nd Call for Contributions and Participation: Workshop on HoTT/UF (with FSCD 2017)   Anders Mortberg
• [Agda] Open call for papers: Special Issue on Homotopy Type Theory and Univalent Foundations   Anders Mortberg
• [Agda] FOREIGN GHC pragma triggers parse error   Shin-Cheng Mu
• [Agda] FOREIGN GHC pragma triggers parse error   Shin-Cheng Mu
• [Agda] The 2018 Federated Logic Conference - Workshop Announcement   Andrzej Murawski
• [Agda] type check performance   Ulf Norell
• [Agda] signature for `with' branch   Ulf Norell
• [Agda] signature for `with' branch   Ulf Norell
• [Agda] Using machine integers / Data.Int from Haskell in Agda   Ulf Norell
• [Agda] Agda options   Ulf Norell
• [Agda] about serialization   Ulf Norell
• [Agda] help explaining instance resolution   Ulf Norell
• [Agda] about serialization   Ulf Norell
• [Agda] about serialization   Ulf Norell
• [Agda] about serialization   Ulf Norell
• [Agda] old .agdai   Ulf Norell
• [Agda] Typing.CheckRHS   Ulf Norell
• [Agda] Typing.CheckRHS   Ulf Norell
• [Agda] Difference between parameterized and indexed datatypes   Ulf Norell
• [Agda] Help at propositional equality proof that contains subst.   Ulf Norell
• [Agda] possible unifier bug / explain error messages?   Ulf Norell
• [Agda] constructor injectiveness   Ulf Norell
• [Agda] Standard library mailing list?   Ulf Norell
• [Agda] is divMod slow?   Ulf Norell
• [Agda] is divMod slow?   Ulf Norell
• [Agda] is divMod slow?   Ulf Norell
• [Agda] is divMod slow?   Ulf Norell
• [Agda] timing for agda-prelude gcd   Ulf Norell
• [Agda] summing rationals   Ulf Norell
• [Agda] summing rationals   Ulf Norell
• [Agda] divmod-unique of Agda prelude   Ulf Norell
• [Agda] Instance fields   Ulf Norell
• [Agda] installing/using 2.6.0-207bde6   Ulf Norell
• [Agda] Bezonas helpon !   Ulf Norell
• [Agda] guidelines for reporting internal errors   Ulf Norell
• [Agda] discovering verbosity options   Ulf Norell
• [Agda] failure to solve b/c undecidable? custom meta solvers?   Ulf Norell
• [Agda] Instance arguments vs auto in Idris.   Ulf Norell
• [Agda] Instance arguments vs auto in Idris.   Ulf Norell
• [Agda] Agda's syntax declaration   Ulf Norell
• [Agda] Agda's syntax declaration   Ulf Norell
• [Agda] Agda's syntax declaration   Ulf Norell
• [Agda] Installing libraries   Ulf Norell
• [Agda] How do I check whether an agda term associated with a specific name relies on hole?   Ulf Norell
• [Agda] Printing strings in the emacs mode   Ulf Norell
• [Agda] on `data' declaration   Ulf Norell
• [Agda] `<' reasoning   Ulf Norell
• [Agda] original Nat   Ulf Norell
• [Agda] original Nat   Ulf Norell
• [Agda] Instance fields   Andreas Nuyts
• [Agda] Instance fields   Andreas Nuyts
• [Agda] Proofs about programs explicitly represented in Agda.   Liam O'Connor
• [Agda] Naive person's questions about agda vs. haskell symbol notation   Liam O'Connor
• [Agda] Holes 0.1.0   Owen
• [Agda] VSTTE 2017 - First Call for Papers   Andrei Paskevich
• [Agda] VSTTE 2017 - Second Call for Papers   Andrei Paskevich
• [Agda] VSTTE 2017 - Deadline Extension   Andrei Paskevich
• [Agda] PPDP 2017: Call For Papers   Brigitte Pientka
• [Agda] PPDP 2017: Call For Papers (Abstract 12 May / Paper 19 May)   Brigitte Pientka
• [Agda] PPDP 2017: ** REVISED PAPER DEADLINE 26 May **   Brigitte Pientka
• [Agda] Call for participation: Workshop on Computer-aided Mathematical Proof, Cambridge UK, 10-14 July 2017   Andrew Pitts
• [Agda] First call for talk proposals: Higher-Order Programming with Effects, HOPE 2017   François Pottier
• [Agda] Second call for talk proposals: Higher-Order Programming with Effects, HOPE 2017   François Pottier
• [Agda] Last call for talk proposals: Higher-Order Programming with Effects, HOPE 2017   François Pottier
• [Agda] Proofs about programs explicitly represented in Agda.   K V S Prasad
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Roman
• [Agda] [newbie] universe levels and BUILTIN EQUALITY   Roman
• [Agda] parameters vs indices   Roman
• [Agda] Trying to load modules from Norell OPLSS tutorial   Manny Romero
• [Agda] Trying to load modules from Norell OPLSS tutorial   Manny Romero
• [Agda] Trying to load modules from Norell OPLSS tutorial   Manny Romero
• [Agda] Trying to load modules from Norell OPLSS tutorial   Manny Romero
• [Agda] How safe is Type:Type?   Gabriel Scherer
• [Agda] how do I handle absurd with patterns?   Carter Schonwald
• [Agda] ICFP 2017 Student Research Competition: Call for Submissions   Sergey, Ilya
• [Agda] CoqPL'18: call for participations and final programme   Sergey, Ilya
• [Agda] How safe is Type:Type?   Michael Shulman
• [Agda] [ANNOUNCE] Agda 2.5.2   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.2   Andrés Sicard-Ramírez
• [Agda] Agda installation for all users   Andrés Sicard-Ramírez
• [Agda] How safe is Type:Type?   Andrés Sicard-Ramírez
• [Agda] Agda options   Andrés Sicard-Ramírez
• [Agda] infix ∸-mono ?   Andrés Sicard-Ramírez
• [Agda] strange mismatch   Andrés Sicard-Ramírez
• [Agda] strange mismatch   Andrés Sicard-Ramírez
• [Agda] strange mismatch   Andrés Sicard-Ramírez
• [Agda] address in lib pull request   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.3 release candidate 1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.3 release candidate 1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.3 release candidate 1   Andrés Sicard-Ramírez
• [Agda] Typechecking with multiple concurrent agda processes.   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.3   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.3   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.3   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.5.3   Andrés Sicard-Ramírez
• [Agda] [REQUEST] Help with transition from 2.5.1/2 (std-lib 0.12) to 2.5.3 (std-lib 0.14)   Andrés Sicard-Ramírez
• [Agda] Trying to load modules from Norell OPLSS tutorial   Andrés Sicard-Ramírez
• [Agda] Trying to load modules from Norell OPLSS tutorial   Andrés Sicard-Ramírez
• [Agda] Trying to load modules from Norell OPLSS tutorial   Andrés Sicard-Ramírez
• [Agda] problems installing agda master using stack   Andrés Sicard-Ramírez
• [Agda] problems installing agda master using stack   Andrés Sicard-Ramírez
• [Agda] Disappearing unicode in Literate Agda - XeLatex   Andrés Sicard-Ramírez
• [Agda] Disappearing unicode in Literate Agda - XeLatex   Andrés Sicard-Ramírez
• [Agda] How safe is Type:Type?   Matthieu Sozeau
• [Agda] How safe is Type:Type?   Matthieu Sozeau
• [Agda] Can intuitionistic type theory express derivations of physical equations more strictly?   Bas Spitters
• [Agda] decidable equality in algebra   Bas Spitters
• [Agda] Adding "print" to TC monad?   Jon Sterling
• [Agda] matching against _::_ ?   Sandro Stucki
• [Agda] Cannot apply injectivity   Sandro Stucki
• [Agda] Cannot apply injectivity   Sandro Stucki
• [Agda] `with' in standard functions   Sandro Stucki
• [Agda] `<' reasoning   Sandro Stucki
• [Agda] How to get rid of warning   Sandro Stucki
• [Agda] Request of suggestion of learning material for Agda   Aaron Stump
• [Agda] 6 Assistant professor positions at the University of Utrecht   Wouter Swierstra
• [Agda] Irrelevance and resurrection in type signatures   Matus Tejiscak
• [Agda] FLOPS2018: First CFP   Peter Thiemann
• [Agda] ARCADE Call for Papers   Dmitriy Traytel
• [Agda] EUTYPES summer school in Ohrid, call for applications   Tarmo Uustalu
• [Agda] Fixpoint in Agda   Marco Vassena
• [Agda] example with insertion to list   Andrea Vezzosi
• [Agda] example with insertion to list   Andrea Vezzosi
• [Agda] Propositional equality for coinductive records   Andrea Vezzosi
• [Agda] Propositional equality for coinductive records   Andrea Vezzosi
• [Agda] Trouble with sizes   Andrea Vezzosi
• [Agda] making a pair explodes   Andrea Vezzosi
• [Agda] making a pair explodes   Andrea Vezzosi
• [Agda] Help at propositional equality proof that contains subst.   Andrea Vezzosi
• [Agda] Caching [Re: Type checking times and a solution.]   Andrea Vezzosi
• [Agda] Caching [Re: Type checking times and a solution.]   Andrea Vezzosi
• [Agda] Possibly infinite/exponential compilation time by just calling a certain function   Andrea Vezzosi
• [Agda] Proposed notation for universe polymorphism   Andrea Vezzosi
• [Agda] [ cubical ] : Questions on PathP on Sets.   Andrea Vezzosi
• [Agda] Should we create an issue to track the status of Cubical?   Andrea Vezzosi
• [Agda] [REQUEST] Help with transition from 2.5.1/2 (std-lib 0.12) to 2.5.3 (std-lib 0.14)   Andrea Vezzosi
• [Agda] Agda's syntax declaration   Andrea Vezzosi
• [Agda] Agda's syntax declaration   Andrea Vezzosi
• [Agda] is divMod slow?   Jorn van Wijk
• [Agda] Some proofs by clauses   James Wood
• [Agda] `let' in function signature   James Wood
• [Agda] PEPM 2018 Call for Papers   PEPM Workshop
• [Agda] PEPM 2018 Final Call for Papers   PEPM Workshop
• [Agda] PEPM 2018 Call for Poster/Demo Abstracts and Participation   PEPM Workshop
• [Agda] PEPM 2018 Final Call for Poster/Demo Abstracts and Participation   PEPM Workshop
• [Agda] I am failing at Sized types 2.   Apostolis Xekoukoulotakis
• [Agda] Removing a deducible Size constrain leads to error.   Apostolis Xekoukoulotakis
• [Agda] Sized types unification error.   Apostolis Xekoukoulotakis
• [Agda] Sized types unification error.   Apostolis Xekoukoulotakis
• [Agda] Propositional equality for coinductive records   Apostolis Xekoukoulotakis
• [Agda] Many ways to open a module - Is there a reason?   Apostolis Xekoukoulotakis
• [Agda] Many ways to open a module - Is there a reason?   Apostolis Xekoukoulotakis
• [Agda] pattern matching order   Apostolis Xekoukoulotakis
• [Agda] Case split creates too many {_}   Apostolis Xekoukoulotakis
• [Agda] Printing named arguments [Re: Case split creates too many {_}]   Apostolis Xekoukoulotakis
• [Agda] Some suggestions for the 'where' syntax and C-c C-,   Apostolis Xekoukoulotakis
• [Agda] Some suggestions for the 'where' syntax and C-c C-,   Apostolis Xekoukoulotakis
• [Agda] Help at propositional equality proof that contains subst.   Apostolis Xekoukoulotakis
• [Agda] Help at propositional equality proof that contains subst.   Apostolis Xekoukoulotakis
• [Agda] Help at propositional equality proof that contains subst.   Apostolis Xekoukoulotakis
• [Agda] Help at propositional equality proof that contains subst.   Apostolis Xekoukoulotakis
• [Agda] Help at propositional equality proof that contains subst.   Apostolis Xekoukoulotakis
• [Agda] 1-infix-2   Apostolis Xekoukoulotakis
• [Agda] Type checking times and a solution.   Apostolis Xekoukoulotakis
• [Agda] Caching [Re: Type checking times and a solution.]   Apostolis Xekoukoulotakis
• [Agda] When catchall does not help.   Apostolis Xekoukoulotakis
• [Agda] When catchall does not help.   Apostolis Xekoukoulotakis
• [Agda] ⊥-elim and proof duplication. Is there another way?   Apostolis Xekoukoulotakis
• [Agda] ⊥-elim and proof duplication. Is there another way?   Apostolis Xekoukoulotakis
• [Agda] email list reference   Apostolis Xekoukoulotakis
• [Agda] Typechecking with multiple concurrent agda processes.   Apostolis Xekoukoulotakis
• [Agda] Typechecking with multiple concurrent agda processes.   Apostolis Xekoukoulotakis
• [Agda] Typechecking with multiple concurrent agda processes.   Apostolis Xekoukoulotakis
• [Agda] [ cubical ] : Questions on PathP on Sets.   Apostolis Xekoukoulotakis
• [Agda] [ cubical ] : Questions on PathP on Sets.   Apostolis Xekoukoulotakis
• [Agda] Should we create an issue to track the status of Cubical?   Apostolis Xekoukoulotakis
• [Agda] `with' in standard functions   Apostolis Xekoukoulotakis
• [Agda] Help with With-permutations.   Apostolis Xekoukoulotakis
• [Agda] Help with With-permutations.   Apostolis Xekoukoulotakis
• [Agda] Instance arguments vs auto in Idris.   Apostolis Xekoukoulotakis
• [Agda] Instance arguments vs auto in Idris.   Apostolis Xekoukoulotakis
• [Agda] Instance arguments vs auto in Idris.   Apostolis Xekoukoulotakis
• [Agda] instance arguments and negation.   Apostolis Xekoukoulotakis
• [Agda] Autumn school "Proof and Computation"   Chuangjie Xu
• [Agda] Autumn school "Proof and Computation"   Chuangjie Xu
• [Agda] CFP: Workshop on Type-driven Development (TyDe '17)   Brent Yorgey
• [Agda] 2nd CFP: Workshop on Type-driven Development (TyDe '17)   Brent Yorgey
• [Agda] Final CFP: Workshop on Type-driven Development (TyDe '17)   Brent Yorgey
• [Agda] LOLA 2017: Call for Talk Proposals   Noam Zeilberger
• [Agda] productivity of fibonacci stream   Noam Zeilberger
• [Agda] productivity of fibonacci stream   Noam Zeilberger
• [Agda] Installing libraries   a.j.rouvoet
• [Agda] 1st Call for Papers IFL 2017   jurriaanhage at gmail.com
• [Agda] 1st CfP: IFL 2017 (29th Symposium on Implementation and Application of Functional Languages)   publicityifl at gmail.com
• [Agda] 2nd CfP: IFL 2017 (29th Symposium on Implementation and Application of Functional Languages)   publicityifl at gmail.com
• [Agda] Extended deadline: IFL 2017 (29th Symposium on Implementation and Application of Functional Languages)   publicityifl at gmail.com
• [Agda] summing rationals   mechvel at scico.botik.ru
• [Agda] Postdoc positions available for ERC "CoqHoTT"   nicolas tabareau
• [Agda] Difference between parameterized and indexed datatypes   v0id_NULL
• [Agda] Some proofs by clauses   v0id_NULL
• [Agda] Some problems with K-S basis   v0id_NULL
• [Agda] Some problems with K-S basis   v0id_NULL
• [Agda] Using machine integers / Data.Int from Haskell in Agda   stvienna wiener
• [Agda] Fix emacs compile hook after updating to new agda version   stvienna wiener
• [Agda] No Agda AIM meeting any more?   stvienna wiener

Last message date: Sun Dec 31 17:07:28 CET 2017
Archived on: Sun Dec 31 17:07:31 CET 2017

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