2015 Archives by author

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

Starting: Thu Jan 1 18:57:31 CEST 2015
Ending: Thu Dec 31 20:03:18 CEST 2015
Messages: 1034

• [Agda] Inspect.   Andrés Sicard-Ramírez
• Re: [Agda] ... n ∸ m > 0   Andrés Sicard-Ramírez
• Re: [Agda] ... n ∸ m > 0   Andrés Sicard-Ramírez
• [Agda] Univalence via Agda's primTrustMe?   Andrés Sicard-Ramírez
• [Agda] printed goal type   Andrés Sicard-Ramírez
• [Agda] `Respects'   Andrés Sicard-Ramírez
• [Agda] Wrong reporting error ? (Was question on `compare')   Andrés Sicard-Ramírez
• [Agda] Wrong reporting error ? (Was question on `compare')   Andrés Sicard-Ramírez
• [Agda] Poll: Remove the Agda interactive mode   Andrés Sicard-Ramírez
• [Agda] Poll: Remove the Agda interactive mode   Andrés Sicard-Ramírez
• [Agda] Fin n -> Fin n extensional?   Andrés Sicard-Ramírez
• [Agda] Fin n -> Fin n extensional?   Andrés Sicard-Ramírez
• [Agda] --termination-depth   Andrés Sicard-Ramírez
• [Agda] --termination-depth   Andrés Sicard-Ramírez
• [Agda] --termination-depth   Andrés Sicard-Ramírez
• [Agda] +-mono arguments   Andrés Sicard-Ramírez
• [Agda] +-mono arguments   Andrés Sicard-Ramírez
• [Agda] Poll: Remove the Epic back-end   Andrés Sicard-Ramírez
• [Agda] Agda 2.4.2.2: Bumped upper version bound for hashtables   Andrés Sicard-Ramírez
• [Agda] Positive but not strictly positive types   Andrés Sicard-Ramírez
• [Agda] Positive but not strictly positive types   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.2   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Andrés Sicard-Ramírez
• [Agda] Re: ANNOUNCE: Agda 2.4.2.3 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.3 release   Andrés Sicard-Ramírez
• [Agda] Parameterized modules   Andrés Sicard-Ramírez
• [Agda] installing agda-2.4.2.3   Andrés Sicard-Ramírez
• [Agda] installing agda-2.4.2.3   Andrés Sicard-Ramírez
• [Agda] Stop creating or modifying issues in Google Code   Andrés Sicard-Ramírez
• [Agda] New bug tracker for Agda   Andrés Sicard-Ramírez
• [Agda] change in operator syntax   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.4 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.4 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.4 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.4 release candidate   Andrés Sicard-Ramírez
• [Agda] unused values   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Standard library 0.10   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.4.2.4   Andrés Sicard-Ramírez
• [Agda] --sharing   Andrés Sicard-Ramírez
• [Agda] Where did "agda2 include dirs" go?   Andrés Sicard-Ramírez
• [Agda] Where did "agda2 include dirs" go?   Andrés Sicard-Ramírez
• [Agda] -1 as identifier   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Standard library 0.11   Andrés Sicard-Ramírez
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Andrés Sicard-Ramírez
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Andrés Sicard-Ramírez
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Andrés Sicard-Ramírez
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Andrés Sicard-Ramírez
• [Agda] Komencenta demando.   Andrés Sicard-Ramírez
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Andrés Sicard-Ramírez
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.4.2.5   Andrés Sicard-Ramírez
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] how to run helloworld in agda   Andrés Sicard-Ramírez
• [Agda] Is it possible to switch off universes checking?   Andrés Sicard-Ramírez
• [Agda] Is it possible to switch off universes checking?   Andrés Sicard-Ramírez
• [Agda] Is it possible to switch off universes checking?   Andrés Sicard-Ramírez
• [Agda] command line type checker vs interactive   Andrés Sicard-Ramírez
• [Agda] command line type checker vs interactive   Andrés Sicard-Ramírez
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   Dr. ÉRDI Gergő
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Dr. ÉRDI Gergő
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Dr. ÉRDI Gergő
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Dr. ÉRDI Gergő
• [Agda] FYI: Rationals in Idris   Dr. ÉRDI Gergő
• [Agda] Positive but not strictly positive types   Frédéric Blanqui
• [Agda] Positive but not strictly positive types   Frédéric Blanqui
• [Agda] Poll: Remove the Agda interactive mode   Håkon Robbestad Gylterud
• [Agda] Positive but not strictly positive types   Vilhelm Sjöberg
• [Agda] Fin n -> Fin n extensional?   João Paulo Pizani Flor
• [Agda] Mathematics of Program Construction (MPC 2015): final call for papers   José Pedro Magalhães
• [Agda] Releasing app with bundled Agda   Marko Koležnik
• [Agda] Releasing app with bundled Agda   Marko Koležnik
• [Agda] Agda master is anti-classical, injective type constructors are back   Andreas Abel
• [Agda] Agda master is anti-classical, injective type constructors are back   Andreas Abel
• [Agda] printed goal type   Andreas Abel
• Heterogeneous pattern matching incompatible with univalence [Re: [Agda] Agda master is anti-classical, injective type constructors are back]   Andreas Abel
• [Agda] Mutual data definitions   Andreas Abel
• [Agda] Wrong reporting error ? (Was question on `compare')   Andreas Abel
• [Agda] Wrong reporting error ? (Was question on `compare')   Andreas Abel
• [Agda] Wrong reporting error ? (Was question on `compare')   Andreas Abel
• [Agda] Inheriting fields   Andreas Abel
• [Agda] Indentation in stdlib files   Andreas Abel
• [Agda] Poll: Remove the Agda interactive mode   Andreas Abel
• [Agda] Re: Forall and product   Andreas Abel
• [Agda] AIM XIX 3-9 June 2015: Save the date!   Andreas Abel
• [Agda] Fin n -> Fin n extensional?   Andreas Abel
• [Agda] Fin n -> Fin n extensional?   Andreas Abel
• [Agda] Re: Forall and product   Andreas Abel
• [Agda] Re: Forall and product   Andreas Abel
• [Agda] PhD position in dependent types/functional programming at Chalmers   Andreas Abel
• [Agda] PhD position in dependent types/functional programming at Chalmers   Andreas Abel
• [Agda] PhD position in dependent types/functional programming at Chalmers   Andreas Abel
• [Agda] --termination-depth   Andreas Abel
• [Agda] Help, I'm failing at sized types.   Andreas Abel
• [Agda] Help, I'm failing at sized types.   Andreas Abel
• [Agda] Help, I'm failing at sized types.   Andreas Abel
• [Agda] Positive but not strictly positive types   Andreas Abel
• [Agda] Re: Implicit arguments   Andreas Abel
• [Agda] Sane whitespace with agda --latex   Andreas Abel
• [Agda] Sane whitespace with agda --latex   Andreas Abel
• [Agda] FLOPS 2016 CFP   Andreas Abel
• [Agda] LFMTP abstracts due 1st May   Andreas Abel
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Andreas Abel
• [Agda] Absurd patterns inconsistent with function extensionality   Andreas Abel
• [Agda] Can't build index.html in HoTT-Agda repository   Andreas Abel
• [Agda] Re: Can't build index.html in HoTT-Agda repository   Andreas Abel
• [Agda] Can't build index.html in HoTT-Agda repository   Andreas Abel
• [Agda] Can't build index.html in HoTT-Agda repository   Andreas Abel
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Andreas Abel
• [Agda] ANNOUNCE: Agda 2.4.2.2   Andreas Abel
• [Agda] Re: ANNOUNCE: Agda 2.4.2.3 release candidate   Andreas Abel
• [Agda] Re: ANNOUNCE: Agda 2.4.2.3 release candidate   Andreas Abel
• [Agda] Reminder: Agda meeting 3-9 June in Gothenburg, call for participation   Andreas Abel
• [Agda] Type a = Set a   Andreas Abel
• [Agda] instance argument problems   Andreas Abel
• [Agda] Parameterized modules   Andreas Abel
• [Agda] Strange behaviour of instance search.   Andreas Abel
• [Agda] Associativity and Heterogeneous Equality   Andreas Abel
• [Agda] Associativity and Heterogeneous Equality   Andreas Abel
• [Agda] Agda dies trying to prove transitivity   Andreas Abel
• Positivity checker performance [Re: [Agda] Agda dies trying to prove transitivity]   Andreas Abel
• Positivity checker performance [Re: [Agda] Agda dies trying to prove transitivity]   Andreas Abel
• [Agda] Associativity and Heterogeneous Equality   Andreas Abel
• [Agda] Associativity and Heterogeneous Equality   Andreas Abel
• [Agda] symbol for a singleton set   Andreas Abel
• [Agda] Should not _ patterns be resolvable by inaccessible patterns?   Andreas Abel
• [Agda] Should not _ patterns be resolvable by inaccessible patterns?   Andreas Abel
• [Agda] arguments in `data' pattern   Andreas Abel
• [Agda] Should not _ patterns be resolvable by inaccessible patterns?   Andreas Abel
• [Agda] segmentation fault   Andreas Abel
• [Agda] Should not _ patterns be resolvable by inaccessible patterns?   Andreas Abel
• [Agda] question about a form of irrelevance elimination   Andreas Abel
• [Agda] where definitions and with   Andreas Abel
• [Agda] Re: where definitions and with   Andreas Abel
• [Agda] Overloading atoms and operators   Andreas Abel
• [Agda] Overloading atoms and operators   Andreas Abel
• [Agda] Renaming of a module, associated with a record, doesn't hide the original name.   Andreas Abel
• [Agda] Renaming of a module, associated with a record, doesn't hide the original name.   Andreas Abel
• [Agda] Renaming of a module, associated with a record, doesn't hide the original name.   Andreas Abel
• [Agda] Renaming of a module, associated with a record, doesn't hide the original name.   Andreas Abel
• [Agda] simple with->case fail   Andreas Abel
• [Agda] Perplexed in a proof   Andreas Abel
• [Agda] FLOPS 2016 last cfp (deadline 21st Sep)   Andreas Abel
• [Agda] ANNOUNCE: Agda 2.4.2.4 release candidate   Andreas Abel
• [Agda] Agda Questions.   Andreas Abel
• No help with homework on this list [Re: [Agda] Agda Questions.]   Andreas Abel
• [Agda] modules named `_`   Andreas Abel
• [Agda] Inconsistent rewrite behavior   Andreas Abel
• [Agda] Inconsistent rewrite behavior   Andreas Abel
• [Agda] Coinductive types and 'duals' to dependent lambda calculus?   Andreas Abel
• [Agda] [ANNOUNCE] Standard library 0.11   Andreas Abel
• [Agda] Type Mismatch in with   Andreas Abel
• [Agda] Reasoning with Pattern Match with Default Cases   Andreas Abel
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Andreas Abel
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Andreas Abel
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Andreas Abel
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Andreas Abel
• More agressive `with` in Agda 2.4.3 [Re: [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!]   Andreas Abel
• [Agda] Komencenta demando.   Andreas Abel
• [Agda] trouble with let and where   Andreas Abel
• [Agda] trouble with let and where   Andreas Abel
• [Agda] trouble with let and where   Andreas Abel
• [Agda] Komencenta demando.   Andreas Abel
• [Agda] Komencenta demando.   Andreas Abel
• [Agda] how to run helloworld in agda   Andreas Abel
• [Agda] FYI: Rationals in Idris   Andreas Abel
• [Agda] a puzzle about pattern matching   Matteo Acerbi
• [Agda] a puzzle about pattern matching   Matteo Acerbi
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Matteo Acerbi
• [Agda] Quotient types in Agda, if you Trust Me   Matteo Acerbi
• [Agda] Quotient types in Agda, if you Trust Me   Matteo Acerbi
• [Agda] Heterogeneous equality of pairs and records: some questions.   Matteo Acerbi
• [Agda] Heterogeneous equality of pairs and records: some questions.   Matteo Acerbi
• [Agda] Heterogeneous equality of pairs and records: some questions.   Matteo Acerbi
• [Agda] Heterogeneous equality of pairs and records: some questions.   Matteo Acerbi
• [Agda] [TFP 2015] 2nd call for papers   Peter Achten
• [Agda] [TFPIE 2015] 2nd call for papers   Peter Achten
• [Agda] [TFP'15] final call for papers - extended deadline march 31 -   Peter Achten
• [Agda] [TFP'15] call for participation   Peter Achten
• [Agda] Using .Xcompose file on Fedora 21   Colin Adams
• [Agda] Using .Xcompose file on Fedora 21   Colin Adams
• [Agda] Can't build index.html in HoTT-Agda repository   Colin Adams
• [Agda] Can't build index.html in HoTT-Agda repository   Colin Adams
• [Agda] Can't build index.html in HoTT-Agda repository   Colin Adams
• [Agda] Using .Xcompose file on Fedora 21   Colin Adams
• [Agda] `Respects'   Arseniy Alekseyev
• [Agda] new use for literate agda!   Thorsten Altenkirch
• [Agda] Fin n -> Fin n extensional?   Thorsten Altenkirch
• [Agda] Fin n -> Fin n extensional?   Thorsten Altenkirch
• [Agda] Re: Forall and product   Thorsten Altenkirch
• [Agda] Re: Forall and product   Thorsten Altenkirch
• [Agda] Midlands Graduate School 2015   Thorsten Altenkirch
• [Agda] Positive but not strictly positive types   Thorsten Altenkirch
• [Agda] Positive but not strictly positive types   Thorsten Altenkirch
• [Agda] Positive but not strictly positive types   Thorsten Altenkirch
• [Agda] Positive but not strictly positive types   Thorsten Altenkirch
• [Agda] Positive but not strictly positive types   Thorsten Altenkirch
• [Agda] PhD studentship in Nottingham available   Thorsten Altenkirch
• [Agda] Quotient types in Agda, if you Trust Me   Thorsten Altenkirch
• [Agda] Quotient types in Agda, if you Trust Me   Thorsten Altenkirch
• [Agda] Type a = Set a   Thorsten Altenkirch
• [Agda] Type a = Set a   Thorsten Altenkirch
• [Agda] agda slow   Thorsten Altenkirch
• [Agda] agda slow   Thorsten Altenkirch
• [Agda] HOTT-style reals in Agda   Thorsten Altenkirch
• [Agda] question about a form of irrelevance elimination   Thorsten Altenkirch
• [Agda] Coinductive types and 'duals' to dependent lambda calculus?   Thorsten Altenkirch
• [Agda] PhD studentships at the Functional Programming Lab in Nottingham   Thorsten Altenkirch
• [Agda] trouble with let and where   Thorsten Altenkirch
• [Agda] Why no impredicative prop?   Thorsten Altenkirch
• [Agda] Why no impredicative prop?   Thorsten Altenkirch
• [Agda] Type a = Set a   Alexander Altman
• [Agda] Agda Questions.   Ismail Alyassiri
• [Agda] Fin n -> Fin n extensional?   Abhishek Anand
• [Agda] Fin n -> Fin n extensional?   Abhishek Anand
• [Agda] Strictly positive   Kenichi Asai
• [Agda] documents on the implementation of agda2-mode?   Kenichi Asai
• [Agda] Re: Associativity and Heterogeneous Equality   Kenichi Asai
• [Agda] mutual recursion on vectors?   Kenichi Asai
• [Agda] MSFP 2016: Call for Papers   Bob Atkey
• [Agda] Bundlling Agda with agda-writer   Andrej Bauer
• [Agda] Agda Writer - a GUI for Agda on OS X   Andrej Bauer
• [Agda] Permanent position at the University of Sussex   Martin Berger
• [Agda] PhD scholarship on foundations of meta-programming   Martin Berger
• [Agda] Parameterized modules   Bruno Bianchi
• [Agda] Parameterized modules   Bruno Bianchi
• [Agda] Sized Natural Numbers   Bruno Bianchi
• [Agda] Sized Natural Numbers   Bruno Bianchi
• [Agda] HOTT-style reals in Agda   Joachim Breitner
• [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?   Guillaume Brunerie
• [Agda] Komencenta demando.   Guillaume Brunerie
• [Agda] CFP: ACM SIGPLAN GPCE 2015   Faruk Caglar
• [Agda] Deadline Approaching - CFP: ACM SIGPLAN GPCE 2015   Faruk Caglar
• [Agda] where definitions and with   Guillermo Calderon
• [Agda] Re: where definitions and with   Guillermo Calderon
• [Agda] Termination checking (perhaps could be smarter)   Carlos Camarao
• [Agda] Termination checking (perhaps could be smarter)   Carlos Camarao
• [Agda] Set properties   Carlos Camarao
• [Agda] Set properties   Carlos Camarao
• [Agda] Fin n -> Fin n extensional?   Jacques Carette
• [Agda] Fin n -> Fin n extensional?   Jacques Carette
• [Agda] Re: Accessing fields of algebra records   Jacques Carette
• [Agda] HoTT-Agda question   Jacques Carette
• [Agda] HoTT-Agda question   Jacques Carette
• [Agda] a puzzle about pattern matching   Jacques Carette
• [Agda] installing agda-2.4.2.3   Jacques Carette
• [Agda] Explain this strange effect from the order of arguments (and provide a workaround, if possible)   Jacques Carette
• [Agda] type check cost for `open'   Jacques Carette
• [Agda] Why no impredicative prop?   Timothy Carstens
• [Agda] Why no impredicative prop?   Timothy Carstens
• [Agda] Why no impredicative prop?   Timothy Carstens
• [Agda] Mutual data definitions   James Chapman
• [Agda] How to install Epic for Agda?   Jesper Cockx
• [Agda] How to install Epic for Agda?   Jesper Cockx
• [Agda] Re: Builtins   Jesper Cockx
• [Agda] Re: Builtins   Jesper Cockx
• [Agda] AIM XXII: proposed date   Jesper Cockx
• [Agda] Agda meeting 16-22 September in Leuven, call for participation   Jesper Cockx
• [Agda] Reminder: AIM XXII is in one month!   Jesper Cockx
• [Agda] Last few remarks before AIM XXII   Jesper Cockx
• [Agda] Where did "agda2 include dirs" go?   Jesper Cockx
• [Agda] Where did "agda2 include dirs" go?   Jesper Cockx
• [Agda] type annotation in-place   Jesper Cockx
• [Agda] type annotation in-place   Jesper Cockx
• [Agda] type annotation in-place   Jesper Cockx
• [Agda] Polymorphism is not (always) naturality   Jesper Cockx
• [Agda] Reasoning with Pattern Match with Default Cases   Jesper Cockx
• [Agda] Reasoning with Pattern Match with Default Cases   Jesper Cockx
• [Agda] trouble with let and where   Jesper Cockx
• [Agda] More heterogeneous equality.   Jesper Cockx
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Jesper Cockx
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Jesper Cockx
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Jesper Cockx
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Jesper Cockx
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Jesper Cockx
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Jesper Cockx
• [Agda] HOTT-style reals in Agda   Jason Dagit
• [Agda] Termination checking (perhaps could be smarter)   Nils Anders Danielsson
• [Agda] pointwise congr.of ++   Nils Anders Danielsson
• [Agda] PhD student, dependent types/functional programming, Chalmers   Nils Anders Danielsson
• [Agda] Re: Accessing fields of algebra records   Nils Anders Danielsson
• [Agda] Re: Accessing fields of algebra records   Nils Anders Danielsson
• [Agda] fast DecTotalOrder   Nils Anders Danielsson
• [Agda] fast DecTotalOrder   Nils Anders Danielsson
• [Agda] fast DecTotalOrder   Nils Anders Danielsson
• [Agda] type check performance   Nils Anders Danielsson
• [Agda] type check performance   Nils Anders Danielsson
• [Agda] type check performance   Nils Anders Danielsson
• [Agda] A problem with instance arguments and function application.   Nils Anders Danielsson
• [Agda] Lit Agda and MMM mode   Nils Anders Danielsson
• [Agda] URLs in comments   Nils Anders Danielsson
• [Agda] Type-preserving renaming and substitutions for a dependently typed lambda calculus.   Nils Anders Danielsson
• [Agda] Re: Builtins   Nils Anders Danielsson
• [Agda] Can't build index.html in HoTT-Agda repository   Nils Anders Danielsson
• [Agda] documents on the implementation of agda2-mode?   Nils Anders Danielsson
• [Agda] literate colours   Nils Anders Danielsson
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Nils Anders Danielsson
• [Agda] agda slow   Nils Anders Danielsson
• [Agda] Strange behaviour of instance search.   Nils Anders Danielsson
• [Agda] Agda dies trying to prove transitivity   Nils Anders Danielsson
• Positivity checker performance [Re: [Agda] Agda dies trying to prove transitivity]   Nils Anders Danielsson
• [Agda] symbol for a singleton set   Nils Anders Danielsson
• [Agda] Overloading atoms and operators   Nils Anders Danielsson
• [Agda] Bundlling Agda with agda-writer   Nils Anders Danielsson
• [Agda] Bundlling Agda with agda-writer   Nils Anders Danielsson
• [Agda] The proving cycle.   Nils Anders Danielsson
• [Agda] The proving cycle.   Nils Anders Danielsson
• [Agda] type check cost   Nils Anders Danielsson
• [Agda] type annotation in-place   Nils Anders Danielsson
• [Agda] type check cost   Nils Anders Danielsson
• [Agda] type check cost   Nils Anders Danielsson
• [Agda] type annotation in-place   Nils Anders Danielsson
• [Agda] type annotation in-place   Nils Anders Danielsson
• [Agda] type check cost   Nils Anders Danielsson
• [Agda] Error defining Universe Polymorphism   Nils Anders Danielsson
• [Agda] Agda under emacs   Nils Anders Danielsson
• [Agda] Releasing app with bundled Agda   Nils Anders Danielsson
• [Agda] Releasing app with bundled Agda   Nils Anders Danielsson
• [Agda] Releasing app with bundled Agda   Nils Anders Danielsson
• [Agda] (All P) Respects =pointwise   Nils Anders Danielsson
• [Agda] ITP 2016: Call for papers   Nils Anders Danielsson
• [Agda] Is it possible to switch off universes checking?   Nils Anders Danielsson
• [Agda] Is it possible to switch off universes checking?   Nils Anders Danielsson
• [Agda] modules named `_`   David Darais
• [Agda] modules named `_`   David Darais
• [Agda] Explain this strange effect from the order of arguments (and provide a workaround, if possible)   Martin Stone Davis
• [Agda] A sticky refusal   Martin Stone Davis
• [Agda] A sticky refusal   Martin Stone Davis
• [Agda] Perplexed in a proof   Martin Stone Davis
• [Agda] Inconsistent rewrite behavior   Martin Stone Davis
• [Agda] Inconsistent rewrite behavior   Martin Stone Davis
• [Agda] How to typecheck "How to keep your Neighbours in Order" in the latest version of Agda   Martin Stone Davis
• [Agda] How to typecheck "How to keep your Neighbours in Order" in the latest version of Agda   Martin Stone Davis
• [Agda] Understanding Agda error messages   Martin Stone Davis
• [Agda] Mutual data definitions   Dominique Devriese
• [Agda] Mutual data definitions   Dominique Devriese
• [Agda] Absurd patterns inconsistent with function extensionality   Gabe Dijkstra
• [Agda] Agda Tutorial darcs repo & pandoc backend   Peter Divianszky
• [Agda] ANN: PandocAgda 2.4.3   Peter Divianszky
• [Agda] Fin n -> Fin n extensional?   Dan Doel
• [Agda] Re: Forall and product   Dan Doel
• [Agda] Positive but not strictly positive types   Dan Doel
• [Agda] Positive but not strictly positive types   Dan Doel
• [Agda] Positive but not strictly positive types   Dan Doel
• [Agda] Positive but not strictly positive types   Dan Doel
• [Agda] question about a form of irrelevance elimination   Dan Doel
• [Agda] Polymorphism is not (always) naturality   Dan Doel
• [Agda] Polymorphism is not (always) naturality   Dan Doel
• [Agda] Polymorphism is not (always) naturality   Dan Doel
• [Agda] Builtins   Kirill Elagin
• [Agda] Re: Builtins   Kirill Elagin
• [Agda] Re: Builtins   Kirill Elagin
• [Agda] Re: Builtins   Kirill Elagin
• [Agda] Type a = Set a   Kirill Elagin
• [Agda] CFP: Workshop on Generic Programming 2015 - Deadline May 15   Sebastian Erdweg
• [Agda] Final CFP: Workshop on Generic Programming 2015 - Deadline May 15   Sebastian Erdweg
• [Agda] Deadline extension: Workshop on Generic Programming 2015 - New deadline May 22   Sebastian Erdweg
• [Agda] Re: Forall and product   Martin Escardo
• [Agda] Re: Forall and product   Martin Escardo
• [Agda] Re: Forall and product   Martin Escardo
• [Agda] Re: Forall and product   Martin Escardo
• [Agda] Re: Forall and product   Martin Escardo
• [Agda] Defining large numbers without recursion, with short programs   Martin Escardo
• [Agda] Defining large numbers without recursion, with short programs   Martin Escardo
• [Agda] Defining large numbers without recursion, with short programs   Martin Escardo
• [Agda] Positive but not strictly positive types   Martin Escardo
• [Agda] Positive but not strictly positive types   Martin Escardo
• [Agda] Implicit arguments   Martin Escardo
• [Agda] ANNOUNCE: Agda 2.4.2.2   Martin Escardo
• [Agda] literate colours   Martin Escardo
• [Agda] question about a form of irrelevance elimination   Martin Escardo
• [Agda] question about a form of irrelevance elimination   Martin Escardo
• [Agda] question about a form of irrelevance elimination   Martin Escardo
• [Agda] question about a form of irrelevance elimination   Martin Escardo
• [Agda] using `abstract'   Martin Escardo
• [Agda] Is it possible to switch off universes checking?   Martin Escardo
• [Agda] Is it possible to switch off universes checking?   Martin Escardo
• [Agda] RE: [HoTT] Univalence via Agda's primTrustMe again   Fredrik Nordvall Forsberg
• [Agda] A HoTT-Date with Thorsten Altenkirch at Strathclyde 04.03.15   Fredrik Nordvall Forsberg
• [Coq-Club] [Agda] A HoTT-Date with Thorsten Altenkirch at Strathclyde 04.03.15   Fredrik Nordvall Forsberg
• [Coq-Club] [Agda] A HoTT-Date with Thorsten Altenkirch at Strathclyde 04.03.15   Fredrik Nordvall Forsberg
• [Agda] Strathclyde Chancellor’s Fellowship research positions (5 years)   Fredrik Nordvall Forsberg
• [Agda] AlCoB 2015: extended submission deadline 9 March   GRLMC
• [Agda] Data.Nat.Primality.Prime and irreducibility   Dr. ERDI Gergo
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   Dr. ERDI Gergo
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   Dr. ERDI Gergo
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   Dr. ERDI Gergo
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Dr. ERDI Gergo
• [Agda] SIGPLAN John C Reynolds Doctoral Dissertation Award   Jeremy Gibbons
• [Agda] mutual recursion on vectors?   Oleg Grenrus
• [Agda] Re: How can I prove associativity of vectors?   Helmut Grohne
• [Agda] Univalence via Agda's primTrustMe?   Jason Gross
• [Agda] Univalence via Agda's primTrustMe?   Jason Gross
• [Agda] Univalence via Agda's primTrustMe?   Jason Gross
• [Agda] Univalence via Agda's primTrustMe?   Jason Gross
• [Agda] Fin n -> Fin n extensional?   Jason Gross
• [Agda] Fin n -> Fin n extensional?   Jason Gross
• [Agda] ANNOUNCE: Agda 2.4.2.2   Byron Hale
• [Agda] ANNOUNCE: Agda 2.4.2.2   Byron Hale
• [Agda] ANNOUNCE: Agda 2.4.2.2   Byron Hale
• [Agda] ANNOUNCE: Agda 2.4.2.2   Byron Hale
• [Agda] Implicit arguments   Peter Hancock
• [Agda] how to run helloworld in agda   Peter Hancock
• [Agda] how to run helloworld in agda   Peter Hancock
• [Agda] simple question   Andrew Harris
• [Agda] Reflection and Application terms   Philipp Hausmann
• [Agda] Reflection and Application terms   Philipp Hausmann
• [Agda] Reflection and Application terms   Philipp Hausmann
• [Agda] Reflection and Application terms   Philipp Hausmann
• [Agda] Universe-Heterogeneous tree   Philipp Hausmann
• [Agda] Universe-Heterogeneous tree   Philipp Hausmann
• [Agda] type check cost for `open'   Philipp Hausmann
• [Agda] Bundlling Agda with agda-writer   Philipp Hausmann
• [Agda] CFP: 25th International Conference on Compiler Construction (CC)   Manuel Hermenegildo
• [Agda] ICFP 2015: Final Call for Papers   David Van Horn
• [Agda] ICFP 2015 Call for Participation   David Van Horn
• [Agda] How to define subsemigroups   Harley Eades III
• No help with homework on this list [Re: [Agda] Agda Questions.]   Harley Eades III
• [Agda] Polymorphism is not (always) naturality   Harley Eades III
• [Agda] Agda documentation   Harley Eades III
• [Agda] Type Mismatch in with   Harley Eades III
• [Agda] Type Mismatch in with   Harley Eades III
• [Agda] Why no impredicative prop?   Harley Eades III
• [Agda] record field as Instance Argument   Guillermo Calderon - INCO
• [Agda] Re: record field as Instance Argument   Guillermo Calderon - INCO
• [Agda] A HoTT-Date with Thorsten Altenkirch at Strathclyde 04.03.15   Darius Jahandarie
• [Agda] Univalence via Agda's primTrustMe?   Alan Jeffrey
• [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?   Alan Jeffrey
• [Agda] Univalence via Agda's primTrustMe?   Alan Jeffrey
• [Agda] Univalence via Agda's primTrustMe?   Alan Jeffrey
• [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?   Alan Jeffrey
• [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?   Alan Jeffrey
• [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?   Alan Jeffrey
• [Agda] Univalence via Agda's primTrustMe again   Alan Jeffrey
• [Agda] Re: [HoTT] Univalence via Agda's primTrustMe again   Alan Jeffrey
• [Agda] Re: [HoTT] Univalence via Agda's primTrustMe again   Alan Jeffrey
• [Agda] Re: [HoTT] Univalence via Agda's primTrustMe again   Alan Jeffrey
• [Agda] Univalence via Agda's primTrustMe again^2   Alan Jeffrey
• [Agda] Re: Univalence via Agda's primTrustMe again^2   Alan Jeffrey
• [Agda] Re: [HoTT] Re: Univalence via Agda's primTrustMe again^2   Alan Jeffrey
• [Agda] Associativity and Heterogeneous Equality   Alan Jeffrey
• [Agda] Associativity and Heterogeneous Equality   Alan Jeffrey
• [Agda] Forall and product   Chris Jenkins
• [Agda] Forall and product   Chris Jenkins
• [Agda] Re: Forall and product   Chris Jenkins
• [Agda] record field as Instance Argument   Chris Jenkins
• [Agda] struggling `with'   Christopher Jenkins
• [Agda] type check performance   Wolfram Kahl
• [Agda] type check performance   Wolfram Kahl
• [Agda] type check performance   Wolfram Kahl
• [Agda] Sane whitespace with agda --latex   Wolfram Kahl
• [Agda] type check performance   Wolfram Kahl
• [Agda] change in operator syntax   Wolfram Kahl
• [Agda] type check performance   Wolfram Kahl
• [Agda] type check cost for `open'   Wolfram Kahl
• [Agda] type check cost for `open'   Wolfram Kahl
• [Agda] type check cost   Wolfram Kahl
• [Agda] command line type checker vs interactive   Wolfram Kahl
• [Agda] command line type checker vs interactive   Wolfram Kahl
• [Agda] Post-doctoral position in interactive theorem proving at the University of Iowa   Chantal Keller
• [Agda] ICFP 2015 Student Research Competition: Final Call for Submissions   Andrew Kennedy
• [Agda] Deadline Extension: ICFP 2015 Student Research Competition   Andrew Kennedy
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Sergey Kirgizov
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Sergey Kirgizov
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Sergey Kirgizov
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Sergey Kirgizov
• [Agda] PhD and Postdoc Positions - KWARC, Jacobs University Bremen   Michael Kohlhase
• [Agda] Reflection and Application terms   Pepijn Kokke
• [Agda] Reflection and Application terms   Pepijn Kokke
• [Agda] Poll: Remove the Agda interactive mode   Mateusz Kowalczyk
• [Agda] Sane whitespace with agda --latex   Mateusz Kowalczyk
• [Agda] Sane whitespace with agda --latex   Mateusz Kowalczyk
• [Agda] Sane whitespace with agda --latex   Mateusz Kowalczyk
• [Agda] Can't build index.html in HoTT-Agda repository   Mateusz Kowalczyk
• [Agda] literate colours   Mateusz Kowalczyk
• [Agda] literate colours   Mateusz Kowalczyk
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Mateusz Kowalczyk
• [Agda] Fin n -> Fin n extensional?   Neelakantan Krishnaswami
• [Agda] Fin n -> Fin n extensional?   Neelakantan Krishnaswami
• [Agda] question about a form of irrelevance elimination   Neelakantan Krishnaswami
• [Agda] question about a form of irrelevance elimination   Neelakantan Krishnaswami
• [Agda] ICFP 2016 Call for Workshop and Co-located Event Proposals   Lindsey Kuper
• [Agda] ICFP 2016 Call for Papers   Lindsey Kuper
• [Agda] Re: ICFP 2016 Call for Papers   Lindsey Kuper
• [Agda] Reasoning with Pattern Match with Default Cases   Larrytheliquid
• [Agda] Agda beginner.   Serge Leblanc
• [Agda] Agda beginner.   Serge Leblanc
• [Agda] Agda beginner.   Serge Leblanc
• [Agda] Komencenta demando.   Serge Leblanc
• [Agda] Komencenta demando.   Serge Leblanc
• [Agda] Komencenta demando.   Serge Leblanc
• [Agda] Komencenta demando.   Serge Leblanc
• [Agda] Komencenta demando.   Serge Leblanc
• [Agda] Komencenta demando.   Serge Leblanc
• [Agda] Komencenta demando.   Serge Leblanc
• [Agda] Komencenta demando.   Serge Leblanc
• [Agda] how to run helloworld in agda   John Leo
• [Agda] how to run helloworld in agda   John Leo
• [Agda] how to run helloworld in agda   John Leo
• [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?   Dan Licata
• [Agda] post-doc and visiting positions at wesleyan   Dan Licata
• [Agda] Fin n -> Fin n extensional?   Dan Licata
• [Agda] HoTT-Agda question   Dan Licata
• [Agda] Quotient types in Agda, if you Trust Me   Dan Licata
• [Agda] Quotient types in Agda, if you Trust Me   Dan Licata
• [Agda] Quotient types in Agda, if you Trust Me   Dan Licata
• [Agda] Reminder: CPP deadline is coming up!   Dan Licata
• [Agda] Reasoning with Pattern Match with Default Cases   Dan Licata
• [Agda] Coinductive types and 'duals' to dependent lambda calculus?   Lars Lindqvist
• [Agda] Coinductive types and 'duals' to dependent lambda calculus?   Lars Lindqvist
• [Agda] Coinductive types and 'duals' to dependent lambda calculus?   Lars Lindqvist
• [Agda] CfP: UF/HoTT workshop, Warsaw, 29--30 June, with TLCA 2015   Peter LeFanu Lumsdaine
• [Agda] HoTT/UF workshop at TLCA Warsaw: abstract deadline Apr 15   Peter LeFanu Lumsdaine
• [Agda] question about a form of irrelevance elimination   Peter LeFanu Lumsdaine
• [Agda] question about a form of irrelevance elimination   Peter LeFanu Lumsdaine
• [Agda] NASA Formal Methods 2016   MUNOZ, CESAR (LARC-D320)
• [Agda] how to run helloworld in agda   Martin Mandy
• [Agda] open import public   Leonhard Markert
• [Agda] how to run and test the basic function in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to use monoid solver and how to derive a concept monoid if assume we do not know monoid   Mandy Martino
• [Agda] is there an example of bertus(kant) to define what equality means for type A?   Mandy Martino
• [Agda] how to use monoid solver and how to derive a concept monoid if assume we do not know monoid   Mandy Martino
• [Agda] is there an example to create algebra from congruence distributive variety   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] how to run helloworld in agda   Mandy Martino
• [Agda] FICS'15 Call for papers - Fixed Points in Computer Science (CSL'15 workshop 11+12 sept. 2015)   Ralph Matthes
• [Agda] FICS'15: 2nd call for papers - Fixed Points in Computer Science (CSL'15 workshop 11+12 sept. 2015)   Ralph Matthes
• [Agda] Fin n -> Fin n extensional?   Conor McBride
• [Agda] Help, I'm failing at sized types.   Conor McBride
• [Agda] Help, I'm failing at sized types.   Conor McBride
• [Agda] Help, I'm failing at sized types.   Conor McBride
• [Agda] Help, I'm failing at sized types.   Conor McBride
• [Agda] Help, I'm failing at sized types.   Conor McBride
• [Agda] Strathclyde PhD Position   Conor McBride
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Conor McBride
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Conor McBride
• [Agda] How can we define a type of symmetric binary operations in Agda ?   Conor McBride
• [Agda] enigmatic `with'   Sergei Meshveliani
• [Agda] enigmatic `with'   Sergei Meshveliani
• [Agda] simple question   Sergei Meshveliani
• [Agda] struggling `with'   Sergei Meshveliani
• [Agda] struggling `with'   Sergei Meshveliani
• [Agda] struggling `with'   Sergei Meshveliani
• [Agda] struggling `with'   Sergei Meshveliani
• [Agda] ... n ∸ m > 0   Sergei Meshveliani
• [Agda] ... n ∸ m > 0   Sergei Meshveliani
• [Agda] ... n ∸ m > 0   Sergei Meshveliani
• [Agda] Termination checking (perhaps could be smarter)   Sergei Meshveliani
• [Agda] Termination checking (perhaps could be smarter)   Sergei Meshveliani
• [Agda] Termination checking (perhaps could be smarter)   Sergei Meshveliani
• [Agda] Re: Issue 1402 in agda: Where clauses in rewrite RHS cause internal error   Sergei Meshveliani
• [Agda] printed goal type   Sergei Meshveliani
• [Agda] printed goal type   Sergei Meshveliani
• [Agda] `Respects'   Sergei Meshveliani
• [Agda] `Respects'   Sergei Meshveliani
• [Agda] question on `compare'   Sergei Meshveliani
• [Agda] question on `compare'   Sergei Meshveliani
• [Agda] How to define subsemigroups   Sergei Meshveliani
• [Agda] Re: How to define subsemigroups   Sergei Meshveliani
• [Agda] pointwise congr.of ++   Sergei Meshveliani
• [Agda] --termination-depth   Sergei Meshveliani
• [Agda] --termination-depth   Sergei Meshveliani
• [Agda] Data.Nat.Primality.Prime and irreducibility   Sergei Meshveliani
• [Agda] --termination-depth   Sergei Meshveliani
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   Sergei Meshveliani
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   Sergei Meshveliani
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   Sergei Meshveliani
• [Agda] primality definition   Sergei Meshveliani
• [Agda] Re: primality definition   Sergei Meshveliani
• [Agda] Re: Accessing fields of algebra records   Sergei Meshveliani
• [Agda] Re: Accessing fields of algebra records   Sergei Meshveliani
• [Agda] unused values   Sergei Meshveliani
• [Agda] Decidable _\equiv_   Sergei Meshveliani
• [Agda] Decidable _\equiv_   Sergei Meshveliani
• [Agda] +-mono arguments   Sergei Meshveliani
• [Agda] +-mono arguments   Sergei Meshveliani
• [Agda] fast DecTotalOrder   Sergei Meshveliani
• [Agda] fast DecTotalOrder   Sergei Meshveliani
• [Agda] fast DecTotalOrder   Sergei Meshveliani
• [Agda] fast DecTotalOrder   Sergei Meshveliani
• [Agda] fast DecTotalOrder   Sergei Meshveliani
• [Agda] fast DecTotalOrder   Sergei Meshveliani
• [Agda] fast DecTotalOrder   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] DoCon-A announcement   Sergei Meshveliani
• [Agda] DoCon-A link   Sergei Meshveliani
• [Agda] Agda beginner.   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.3 release candidate   Sergei Meshveliani
• [Agda] Type a = Set a   Sergei Meshveliani
• [Agda] Re: Type a = Set a   Sergei Meshveliani
• [Agda] profiling   Sergei Meshveliani
• [Agda] Associativity and Heterogeneous Equality   Sergei Meshveliani
• [Agda] on parametric modules   Sergei Meshveliani
• [Agda] generic map-cong   Sergei Meshveliani
• [Agda] symbol for a singleton set   Sergei Meshveliani
• [Agda] "Not a valid let-declaration"   Sergei Meshveliani
• [Agda] arguments in `data' pattern   Sergei Meshveliani
• [Agda] segmentation fault   Sergei Meshveliani
• [Agda] installing agda-2.4.2.3   Sergei Meshveliani
• [Agda] installing agda-2.4.2.3   Sergei Meshveliani
• [Agda] installing agda-2.4.2.3   Sergei Meshveliani
• [Agda] installing agda-2.4.2.3   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] change in operator syntax   Sergei Meshveliani
• [Agda] change in operator syntax   Sergei Meshveliani
• [Agda] change in operator syntax   Sergei Meshveliani
• [Agda] type check performance   Sergei Meshveliani
• [Agda] type check cost for `open'   Sergei Meshveliani
• [Agda] type check cost for `open'   Sergei Meshveliani
• [Agda] type check cost for `open'   Sergei Meshveliani
• [Agda] type check cost for `open'   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.4 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.4 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.4 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.4 release candidate   Sergei Meshveliani
• [Agda] agdai size   Sergei Meshveliani
• [Agda] unused values   Sergei Meshveliani
• [Agda] Performance issues with --sharing   Sergei Meshveliani
• [Agda] Performance issues with --sharing   Sergei Meshveliani
• [Agda] Performance issues with --sharing   Sergei Meshveliani
• [Agda] Performance issues with --sharing   Sergei Meshveliani
• [Agda] --sharing   Sergei Meshveliani
• [Agda] using `abstract'   Sergei Meshveliani
• [Agda] type annotation in-place   Sergei Meshveliani
• [Agda] type annotation in-place   Sergei Meshveliani
• [Agda] type annotation in-place   Sergei Meshveliani
• [Agda] type check cost   Sergei Meshveliani
• [Agda] type check cost   Sergei Meshveliani
• [Agda] -1 as identifier   Sergei Meshveliani
• [Agda] type check cost   Sergei Meshveliani
• [Agda] type check cost   Sergei Meshveliani
• [Agda] HO logic   Sergei Meshveliani
• [Agda] Agda under emacs   Sergei Meshveliani
• [Agda] type check cost   Sergei Meshveliani
• [Agda] operator treating   Sergei Meshveliani
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Sergei Meshveliani
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Sergei Meshveliani
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Sergei Meshveliani
• More agressive `with` in Agda 2.4.3 [Re: [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!]   Sergei Meshveliani
• [Agda] trouble with let and where   Sergei Meshveliani
• [Agda] trouble with let and where   Sergei Meshveliani
• [Agda] (All P) Respects =pointwise   Sergei Meshveliani
• [Agda] how to run helloworld in agda   Sergei Meshveliani
• [Agda] how to run helloworld in agda   Sergei Meshveliani
• [Agda] how to run helloworld in agda   Sergei Meshveliani
• [Agda] how to run helloworld in agda   Sergei Meshveliani
• [Agda] FYI: Rationals in Idris   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Sergei Meshveliani
• [Agda] how to use monoid solver and how to derive a concept monoid if assume we do not know monoid   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Sergei Meshveliani
• [Agda] how to run helloworld in agda   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Sergei Meshveliani
• [Agda] ANNOUNCE: Agda 2.4.2.5 release candidate   Sergei Meshveliani
• [Agda] testing unifier   Sergei Meshveliani
• [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] 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] command line type checker vs interactive   Sergei Meshveliani
• [Agda] A new rewrite 'tactic'.   Victor Miraldo
• [Agda] Error defining Universe Polymorphism   Ashish Mishra
• [Agda] Fwd: Error defining Universe Polymorphism   Ashish Mishra
• [Agda] Error defining Universe Polymorphism   Ashish Mishra
• [Agda] Type Checking in Agda   Ashish Mishra
• [Agda] Type Mismatch in with   Ashish Mishra
• [Agda] Type Mismatch in with   Ashish Mishra
• [Agda] Type Mismatch in with   Ashish Mishra
• [Agda] Re: Fin n -> Fin n extensional?   Stefan Monnier
• [Agda] Re: No help with homework on this list [Re: Agda Questions.]   Stefan Monnier
• [Agda] operator treating   Andrew Morris
• [Agda] Agda beginner.   Ulf Norell
• [Agda] A problem with instance arguments and function application.   Ulf Norell
• [Agda] Re: Implicit arguments   Ulf Norell
• [Agda] DoCon-A link   Ulf Norell
• [Agda] agda slow   Ulf Norell
• [Agda] Reflection and Application terms   Ulf Norell
• [Agda] arguments in `data' pattern   Ulf Norell
• [Agda] Should not _ patterns be resolvable by inaccessible patterns?   Ulf Norell
• [Agda] Agda can't find an obvious instance.   Ulf Norell
• [Agda] tweaking evaluation   Ulf Norell
• [Agda] modules named `_`   Ulf Norell
• [Agda] Where did "agda2 include dirs" go?   Ulf Norell
• [Agda] Agda under emacs   Ulf Norell
• [Agda] Agda documentation   Ulf Norell
• [Agda] Reasoning with Pattern Match with Default Cases   Ulf Norell
• [Agda] Reasoning with Pattern Match with Default Cases   Ulf Norell
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   Ulf Norell
• [Agda] how to run helloworld in agda   Ulf Norell
• [Agda] how to run helloworld in agda   Ulf Norell
• [Agda] FYI: Rationals in Idris   Ulf Norell
• [Agda] Is it possible to switch off universes checking?   Ulf Norell
• [Agda] HO logic   Liam O'Connor
• [Agda] Komencenta demando.   Liam O'Connor
• [Agda] My MSc Dissertation   Ali Onaissi
• [Agda] Agda master is anti-classical, injective type constructors are back   Owen
• [Agda] First Call for Papers, PxTP 2015   Andrei Paskevich
• [Agda] Last Call for Papers, PxTP 2015   Andrei Paskevich
• [Agda] Summer School on Generic and Effectful Programming   Maciej Pirog
• [Agda] Univalence via Agda's primTrustMe?   Andrew Pitts
• [Agda] Quotient types in Agda, if you Trust Me   Andrew Pitts
• [Agda] Quotient types in Agda, if you Trust Me   Andrew Pitts
• [Agda] Quotient types in Agda, if you Trust Me   Andrew Pitts
• [Agda] Quotient types in Agda, if you Trust Me   Andrew Pitts
• [Agda] Quotient types in Agda, if you Trust Me   Andrew Pitts
• [Agda] open import public   Andrew Pitts
• [Agda] open import public   Andrew Pitts
• [Agda] instance argument problems   Andrew Pitts
• [Agda] instance argument problems   Andrew Pitts
• [Agda] question about a form of irrelevance elimination   Andrew Pitts
• [Agda] question about a form of irrelevance elimination   Andrew Pitts
• [Agda] question about a form of irrelevance elimination   Andrew Pitts
• [Agda] Bundlling Agda with agda-writer   Andrew Pitts
• [Agda] type annotation in-place   Andrew Pitts
• [Agda] type annotation in-place   Andrew Pitts
• [Agda] Agda documentation   Andrew Pitts
• [Agda] Re: Builtins   Nicolas Pouillard
• [Agda] Using .Xcompose file on Fedora 21   Nicolas Pouillard
• [Agda] Absurd patterns inconsistent with function extensionality   Nicolas Pouillard
• [Agda] Using .Xcompose file on Fedora 21   Nicolas Pouillard
• [Agda] Using .Xcompose file on Fedora 21   Nicolas Pouillard
• [Agda] Type a = Set a   Nicolas Pouillard
• [Agda] Reflection and Application terms   Nicolas Pouillard
• [Agda] Renaming of a module, associated with a record, doesn't hide the original name.   Nicolas Pouillard
• [Agda] change in operator syntax   Nicolas Pouillard
• [Agda] Renaming of a module, associated with a record, doesn't hide the original name.   Nicolas Pouillard
• [Agda] trouble with let and where   Nicolas Pouillard
• [Agda] Inheriting fields   N. Raghavendra
• [Agda] Re: Inheriting fields   N. Raghavendra
• [Agda] Indentation in stdlib files   N. Raghavendra
• [Agda] Re: Indentation in stdlib files   N. Raghavendra
• [Agda] Re: Indentation in stdlib files   N. Raghavendra
• [Agda] How to define subsemigroups   N. Raghavendra
• [Agda] Re: How to define subsemigroups   N. Raghavendra
• [Agda] Re: How to define subsemigroups   N. Raghavendra
• [Agda] Forall and product   N. Raghavendra
• [Agda] Re: Forall and product   N. Raghavendra
• [Agda] Re: Forall and product   N. Raghavendra
• [Agda] Re: Forall and product   N. Raghavendra
• [Agda] Re: Forall and product   N. Raghavendra
• [Agda] Irrationality proof   N. Raghavendra
• [Agda] Re: Irrationality proof   N. Raghavendra
• [Agda] Data.Nat.Primality.Prime and irreducibility   N. Raghavendra
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   N. Raghavendra
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   N. Raghavendra
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   N. Raghavendra
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   N. Raghavendra
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   N. Raghavendra
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   N. Raghavendra
• [Agda] Re: Data.Nat.Primality.Prime and irreducibility   N. Raghavendra
• [Agda] Re: primality definition   N. Raghavendra
• [Agda] Accessing fields of algebra records   N. Raghavendra
• [Agda] Re: Accessing fields of algebra records   N. Raghavendra
• [Agda] Re: Accessing fields of algebra records   N. Raghavendra
• [Agda] Re: Accessing fields of algebra records   N. Raghavendra
• [Agda] Re: Accessing fields of algebra records   N. Raghavendra
• [Agda] Re: Accessing fields of algebra records   N. Raghavendra
• [Agda] Re: Accessing fields of algebra records   N. Raghavendra
• [Agda] Re: Accessing fields of algebra records   N. Raghavendra
• [Agda] Lit Agda and MMM mode   N. Raghavendra
• [Agda] Re: Lit Agda and MMM mode   N. Raghavendra
• [Agda] URLs in comments   N. Raghavendra
• [Agda] Re: URLs in comments   N. Raghavendra
• [Agda] Implicit arguments   N. Raghavendra
• [Agda] Re: Implicit arguments   N. Raghavendra
• [Agda] Re: Implicit arguments   N. Raghavendra
• [Agda] Re: Implicit arguments   N. Raghavendra
• [Agda] Re: Implicit arguments   N. Raghavendra
• [Agda] Builtins   N. Raghavendra
• [Agda] Re: Builtins   N. Raghavendra
• [Agda] Re: Builtins   N. Raghavendra
• [Agda] Re: Builtins   N. Raghavendra
• [Agda] Re: Builtins   N. Raghavendra
• [Agda] Re: Builtins   N. Raghavendra
• [Agda] Re: Can't build index.html in HoTT-Agda repository   N. Raghavendra
• [Agda] Re: Can't build index.html in HoTT-Agda repository   N. Raghavendra
• [Agda] Re: Can't build index.html in HoTT-Agda repository   N. Raghavendra
• [Agda] Fin n -> Fin n extensional?   Gabriel Scherer
• [Agda] Re: Fin n -> Fin n extensional?   Gabriel Scherer
• [Agda] URLs in comments   Gabriel Scherer
• [Agda] Overloading atoms and operators   Gabriel Scherer
• [Agda] Type Checking in Agda   Gabriel Scherer
• [Agda] question on `compare'   Peter Selinger
• [Agda] Fin n -> Fin n extensional?   Peter Selinger
• [Agda] Fin n -> Fin n extensional?   Peter Selinger
• [Agda] Re: Forall and product   Peter Selinger
• [Agda] tweaking evaluation   Peter Selinger
• [Agda] type check cost for `open'   Peter Selinger
• [Agda] type check cost for `open'   Peter Selinger
• [Agda] type check cost for `open'   Peter Selinger
• [Agda] Performance issues with --sharing   Peter Selinger
• [Agda] Performance issues with --sharing   Peter Selinger
• [Agda] Performance issues with --sharing   Peter Selinger
• [Agda] Agda documentation   Peter Selinger
• [Agda] Reasoning with Pattern Match with Default Cases   Peter Selinger
• [Agda] Reasoning with Pattern Match with Default Cases   Peter Selinger
• [Agda] trouble with let and where   Peter Selinger
• [Agda] trouble with let and where   Peter Selinger
• [Agda] trouble with let and where   Peter Selinger
• [Agda] Postdoc positions and lectureships in Swansea (suitable for Agda people; deadlines 22/12/15 and 5/1/16)   Anton Setzer
• [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?   Michael Shulman
• [Agda] Agda master is anti-classical, injective type constructors are back   Matthieu Sozeau
• [Agda] HOTT-style reals in Agda   Bas Spitters
• [Agda] HOTT-style reals in Agda   Bas Spitters
• [Agda] HOTT-style reals in Agda   Bas Spitters
• [Agda] FYI: Rationals in Idris   Bas Spitters
• [Agda] Why no impredicative prop?   Bas Spitters
• [Agda] Why no impredicative prop?   Bas Spitters
• [Agda] Agda beginner.   Dmytro Starosud
• [Agda] Agda beginner.   Dmytro Starosud
• [Agda] Re: Forall and product   Jon Sterling
• [Agda] Fin n -> Fin n extensional?   Jon Sterling
• [Agda] Type a = Set a   Jon Sterling
• [Agda] Agda documentation   Jon Sterling
• [Agda] Komencenta demando.   Jon Sterling
• [Agda] Why no impredicative prop?   Jon Sterling
• [Agda] Why no impredicative prop?   Jon Sterling
• [Agda] Help, I'm failing at sized types.   Jan Stolarek
• [Agda] DSLDI: 3rd Workshop on Domain-Specific Language Design and Implementation   Tijs van der Storm
• [Agda] DSLDI: 3rd Workshop on Domain-Specific Language Design and Implementation (EXTENDED DEADLINE)   Tijs van der Storm
• [Agda] Fin n -> Fin n extensional?   Aaron Stump
• [Agda] Fin n -> Fin n extensional?   Aaron Stump
• [Agda] Fin n -> Fin n extensional?   Aaron Stump
• [Agda] Defining large numbers without recursion, with short programs   Aaron Stump
• [Agda] Positive but not strictly positive types   Aaron Stump
• [Agda] Positive but not strictly positive types   Aaron Stump
• [Agda] Positive but not strictly positive types   Aaron Stump
• [Agda] a puzzle about pattern matching   Aaron Stump
• [Agda] a puzzle about pattern matching   Aaron Stump
• [Agda] Positive but not strictly positive types   Aaron Stump
• [Agda] Agda Questions.   Aaron Stump
• [Agda] Reasoning with Pattern Match with Default Cases   Aaron Stump
• [Agda] PhD positions in Utrecht   Wouter Swierstra
• [Agda] CFP: Special issue of JFP on dependently typed programming   Wouter Swierstra
• [Agda] Agda documentation   Wouter Swierstra
• [Agda] JFP Issue on Dependently typed programming: second call for papers   Wouter Swierstra
• [Agda] Journal of Formalized Reasoning opens a section for PhD/HDR thesis   Enrico Tassi
• [Agda] Agda dies trying to prove transitivity   Peter Thiemann
• [Agda] Agda dies trying to prove transitivity   Peter Thiemann
• [Agda] Termination checking (perhaps could be smarter)   Gregor Ulm
• [Agda] TYPES 2015 call for contributions   Tarmo Uustalu
• [Agda] TYPES 2015 2nd call for contributions   Tarmo Uustalu
• [Agda] TYPES 2015 submission deadline extended   Tarmo Uustalu
• [Agda] TYPES 2015 call for participation   Tarmo Uustalu
• [Agda] TYPES 2015 post-proceedings open call for papers   Tarmo Uustalu
• [Agda] TYPES 2015 post-proceedings open call for papers (reminder)   Tarmo Uustalu
• [Agda] Associativity and Heterogeneous Equality   Marco Vassena
• [Agda] Associativity and Heterogeneous Equality   Marco Vassena
• [Agda] Reasoning with Pattern Match with Default Cases   Marco Vassena
• [Agda] enigmatic `with'   Andrea Vezzosi
• [Agda] struggling `with'   Andrea Vezzosi
• [Agda] struggling `with'   Andrea Vezzosi
• [Agda] Agda master is anti-classical, injective type constructors are back   Andrea Vezzosi
• [Agda] Agda master is anti-classical, injective type constructors are back   Andrea Vezzosi
• [Agda] `Respects'   Andrea Vezzosi
• [Agda] `Respects'   Andrea Vezzosi
• [Agda] Re: [HoTT] Univalence via Agda's primTrustMe again   Andrea Vezzosi
• [Agda] Re: [HoTT] Univalence via Agda's primTrustMe again   Andrea Vezzosi
• [Agda] Re: Forall and product   Andrea Vezzosi
• [Agda] Re: [HoTT] Re: Univalence via Agda's primTrustMe again^2   Andrea Vezzosi
• [Agda] Fin n -> Fin n extensional?   Andrea Vezzosi
• [Agda] Fin n -> Fin n extensional?   Andrea Vezzosi
• [Coq-Club] [Agda] A HoTT-Date with Thorsten Altenkirch at Strathclyde 04.03.15   Andrea Vezzosi
• [Agda] Re: Accessing fields of algebra records   Andrea Vezzosi
• [Agda] Help, I'm failing at sized types.   Andrea Vezzosi
• [Agda] fast DecTotalOrder   Andrea Vezzosi
• [Agda] fast DecTotalOrder   Andrea Vezzosi
• [Agda] type check performance   Andrea Vezzosi
• [Agda] Agda meeting 3-9 June in Gothenburg, call for participation   Andrea Vezzosi
• [Agda] Quotient types in Agda, if you Trust Me   Andrea Vezzosi
• [Agda] Sized Natural Numbers   Andrea Vezzosi
• [Agda] agda slow   Andrea Vezzosi
• [Agda] Sized Natural Numbers   Andrea Vezzosi
• [Agda] agda slow   Andrea Vezzosi
• [Agda] agda slow   Andrea Vezzosi
• [Agda] agda slow   Andrea Vezzosi
• [Agda] Should not _ patterns be resolvable by inaccessible patterns?   Andrea Vezzosi
• [Agda] installing agda-2.4.2.3   Andrea Vezzosi
• [Agda] An Agda proof of the Church-Rosser theorem   Andrea Vezzosi
• [Agda] The proving cycle.   Andrea Vezzosi
• [Agda] change in operator syntax   Andrea Vezzosi
• [Agda] A sticky refusal   Andrea Vezzosi
• [Agda] A sticky refusal   Andrea Vezzosi
• [Agda] type check cost for `open'   Andrea Vezzosi
• [Agda] type check cost   Andrea Vezzosi
• [Agda] type check cost   Andrea Vezzosi
• [Agda] `abstract' fail   Andrea Vezzosi
• [Agda] using `abstract'   Andrea Vezzosi
• [Agda] Polymorphism is not (always) naturality   Andrea Vezzosi
• [Agda] Polymorphism is not (always) naturality   Andrea Vezzosi
• [Agda] Heterogeneous equality of pairs and records: some questions.   Andrea Vezzosi
• [Agda] Polymorphism is not (always) naturality   Andrea Vezzosi
• [Agda] Heterogeneous equality of pairs and records: some questions.   Andrea Vezzosi
• [Agda] Heterogeneous equality of pairs and records: some questions.   Andrea Vezzosi
• [Agda] Heterogeneous equality of pairs and records: some questions.   Andrea Vezzosi
• [Agda] Polymorphism is not (always) naturality   Andrea Vezzosi
• [Agda] Polymorphism is not (always) naturality   Andrea Vezzosi
• [Agda] Understanding Agda error messages   Andrea Vezzosi
• [Agda] trouble with let and where   Andrea Vezzosi
• [Agda] how to run helloworld in agda   Andrea Vezzosi
• [Agda] how to run helloworld in agda   Andrea Vezzosi
• [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?   Vladimir Voevodsky
• [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?   Vladimir Voevodsky
• [Coq-Club] [Agda] A HoTT-Date with Thorsten Altenkirch at Strathclyde 04.03.15   Vladimir Voevodsky
• [Agda] next year memberships at the IAS   Vladimir Voevodsky
• [Agda] 2016-2017 at the IAS   Vladimir Voevodsky
• [Agda] 2016-2017 at the IAS   Vladimir Voevodsky
• [Agda] Re: [Coq-Club] 2016-2017 at the IAS   Vladimir Voevodsky
• [Agda] 2016 Heidelberg Laureates Forum   Vladimir Voevodsky
• [Agda] Mentoring workshop @ ICFP   Stephanie Weirich
• [Agda] AI4FM 2015: Call for Short Contributions   Iain Whiteside
• [Agda] Internship Opportunity at Galois: Winter/Sprint 2016   Ryan Wright
• [Agda] CFP: ACM SIGPLAN GPCE 2015   Mianlai Zhou
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   darais at cs.umd.edu
• [Agda] Defining large numbers without recursion, with short programs   effectfully
• [Agda] A problem with instance arguments and function application.   effectfully
• [Agda] A problem with instance arguments and function application.   effectfully
• [Agda] A problem with instance arguments and function application.   effectfully
• [Agda] Positive but not strictly positive types   effectfully
• [Agda] Positive but not strictly positive types   effectfully
• [Agda] Implicit arguments   effectfully
• [Agda] Re: Implicit arguments   effectfully
• [Agda] a puzzle about pattern matching   effectfully
• [Agda] Type-preserving renaming and substitutions for a dependently typed lambda calculus.   effectfully
• [Agda] Type-preserving renaming and substitutions for a dependently typed lambda calculus.   effectfully
• [Agda] instance argument problems   effectfully
• [Agda] Strange behaviour of instance search.   effectfully
• [Agda] Strange behaviour of instance search.   effectfully
• [Agda] Strange behaviour of instance search.   effectfully
• [Agda] Associativity and Heterogeneous Equality   effectfully
• [Agda] Agda can't find an obvious instance.   effectfully
• [Agda] Agda can't find an obvious instance.   effectfully
• [Agda] Renaming of a module, associated with a record, doesn't hide the original name.   effectfully
• [Agda] Universe-Heterogeneous tree   effectfully
• [Agda] Universe-Heterogeneous tree   effectfully
• [Agda] Universe-Heterogeneous tree   effectfully
• [Agda] Renaming of a module, associated with a record, doesn't hide the original name.   effectfully
• [Agda] Renaming of a module, associated with a record, doesn't hide the original name.   effectfully
• [Agda] Renaming of a module, associated with a record, doesn't hide the original name.   effectfully
• [Agda] The proving cycle.   effectfully
• [Agda] The proving cycle.   effectfully
• [Agda] Lambda terms as a natural transformation.   effectfully
• [Agda] modules named `_`   effectfully
• [Agda] modules named `_`   effectfully
• [Agda] Polymorphism is not (always) naturality   effectfully
• [Agda] How to typecheck "How to keep your Neighbours in Order" in the latest version of Agda   effectfully
• [Agda] How to typecheck "How to keep your Neighbours in Order" in the latest version of Agda   effectfully
• [Agda] Type Checking in Agda   effectfully
• [Agda] Type Checking in Agda   effectfully
• [Agda] Agda documentation   effectfully
• [Agda] Type Mismatch in with   effectfully
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   effectfully
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   effectfully
• [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!   effectfully
• More agressive `with` in Agda 2.4.3 [Re: [Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!]   effectfully
• [Agda] trouble with let and where   effectfully
• [Agda] More heterogeneous equality.   effectfully
• [Agda] More heterogeneous equality.   effectfully
• [Agda] Is it possible to switch off universes checking?   effectfully
• [Agda] Is it possible to switch off universes checking?   effectfully
• [Agda] Is it possible to switch off universes checking?   effectfully
• [Agda] Is it possible to switch off universes checking?   effectfully
• [Agda] simple question   flicky frans
• [Agda] Re: How can I prove associativity of vectors?   flicky frans
• [Agda] Inspect.   flicky frans
• [Agda] Termination checking (perhaps could be smarter)   flicky frans
• [Agda] Termination checking (perhaps could be smarter)   flicky frans
• [Agda] Termination checking (perhaps could be smarter)   flicky frans
• [Agda] Re: Indentation in stdlib files   gallais
• [Agda] Strictly positive   gallais
• [Agda] How to install Epic for Agda?   gallais
• [Agda] --termination-depth   gallais
• [Agda] URLs in comments   gallais
• [Agda] literate colours   gallais
• [Agda] Universe-Heterogeneous tree   gallais
• [Agda] Universe-Heterogeneous tree   gallais
• [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?   maxim.budaev at googlemail.com
• [HoTT] Re: [Agda] Univalence via Agda's primTrustMe?   maxim.budaev at googlemail.com
• [Agda] type check cost for `open'   mechvel at scico.botik.ru
• [Agda] simple with->case fail   mechvel at scico.botik.ru
• [Agda] type check cost   mechvel at scico.botik.ru
• [Agda] type check cost   mechvel at scico.botik.ru
• [Agda] `abstract' fail   mechvel at scico.botik.ru
• [Agda] First Call for Papers for IFL 2015   publicityifl at gmail.com
• [Agda] An Agda proof of the Church-Rosser theorem   roconnor at theorem.ca
• [Agda] An Agda proof of the Church-Rosser theorem   roconnor at theorem.ca

Last message date: Thu Dec 31 20:03:18 CEST 2015
Archived on: Thu Dec 31 20:05:54 CEST 2015

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