2020 Archives by author

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

Starting: Wed Jan 1 13:02:27 CET 2020
Ending: Thu Dec 31 23:40:10 CET 2020
Messages: 966

• [Agda] Multi-line comments in literate Agda files   Uma Zalakain (PGR)
• [Agda] a tutorial for proof by coinduction   Pierre Lescanne (en)
• [Agda] a tutorial for proof by coinduction   Pierre Lescanne (en)
• [Agda] \ell does not display   Pierre Lescanne (en)
• [Agda] Has Agda been tested on i686 architecture ?   Pierre Lescanne (en)
• [Agda] \ell does not display   Pierre Lescanne (en)
• [Agda] Converting intrinsically typed terms   rozowski w.k. (wkr1u18)
• [Agda] Converting intrinsically typed terms   rozowski w.k. (wkr1u18)
• [Agda] Example of an online conference in theoretical computer science BCTCS starting now   Setzer A.G.
• [Agda] Example of an online conference in theoretical computer science BCTCS starting now   Setzer A.G.
• [Agda] Question about colists, musical notation vs coinductive records, and all that   Setzer A.G.
• [Agda] A preliminary programme for AIM XXXII   Setzer A.G.
• [Agda] Getting started: couple more questions   Andreas Abel
• [Agda] PPDP 2020 Call For Papers   Andreas Abel
• [Agda] PPDP 2020 Call For Papers (corrected link)   Andreas Abel
• [Agda] Agda meeting postponed [Fwd: AIM XXXI Postponed]   Andreas Abel
• [Agda] failure of cabal install Agda   Andreas Abel
• [Agda] How can I implement naive sized lambdas?   Andreas Abel
• [Agda] splitting cases   Andreas Abel
• [Agda] L and inverted L characters   Andreas Abel
• [Agda] Strict equality _≣_ in agda   Andreas Abel
• [Agda] Strict equality _≣_ in agda   Andreas Abel
• [Agda] Strict equality _≣_ in agda   Andreas Abel
• [Agda] An article by Jean-Yves Girard   Andreas Abel
• [Agda] Nat Fuel vs Sized Types (and other Sized Type questions)   Andreas Abel
• [Agda] An article by Jean-Yves Girard   Andreas Abel
• [Agda] What do you use for variable binding in 2020?   Andreas Abel
• [Agda] PPDP 2020 Final call for papers   Andreas Abel
• [Agda] how to evaluate in the current context   Andreas Abel
• [Agda] PPDP 2020 deadline extension   Andreas Abel
• [Agda] Performance: opening parameterized modules before the fields of a record   Andreas Abel
• [Agda] Value-recursive records?   Andreas Abel
• [Agda] several agda versions   Andreas Abel
• [Agda] "not in scope" without "does not export"   Andreas Abel
• [Agda] BOPL / PPDP 2020 call for participation (register until 3 Sep)   Andreas Abel
• [Agda] agda2lagda (Halloween edition): Agda for the illiterate   Andreas Abel
• [Agda] [TFP'20] draft paper deadline open (January 10 2020) Trends in Functional Programming 2020, 13-14 February, Krakow, Poland   Peter Achten
• [Agda] [TFP'20] call for participation: Trends in Functional Programming 2020, 13-14 February, Krakow, Poland   Peter Achten
• [Agda] [TFP'21] first call for papers: Trends in Functional Programming 2021, 17-19 February (with Lambda Days 2021 & TFPIE 2021)   Peter Achten
• [Agda] [TFPIE'21] First Call For Papers: Trends in Functional Programming *in Education* 2021, 16 February (with Lambda Days 2021 & TFP 2021)   Peter Achten
• [Agda] [TFP'21] second call for papers: Trends in Functional Programming 2021, 18-19 February (online event with Lambda Days 2021 & TFPIE 2021)   Peter Achten
• [Agda] [TFPIE'21] Second Call For Papers: Trends in Functional Programming *in Education* 2021, 16 February 2021 (with Lambda Days 2021 & TFP 2021)   Peter Achten
• [Agda] Update on Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'20) on July 5-6, 2020   Benedikt Ahrens
• [Agda] PhD position at University of Birmingham, UK   Benedikt Ahrens
• [Agda] Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'20) on July 5-6, 2020   Benedikt Ahrens
• [Agda] Call for Participation: HoTT/UF 2020 - July 5-7   Benedikt Ahrens
• [Agda] [Coq-Club] Why dependent type theory?   Ettore Aldrovandi
• [Agda] [Coq-Club] Why dependent type theory?   Ettore Aldrovandi
• [Agda] [Coq-Club] Why dependent type theory?   Ettore Aldrovandi
• [Agda] Hanging out with the Lean crowd   Ettore Aldrovandi
• [Agda] Problem with generalised variables   G. Allais
• [Agda] Overloaded constructor trouble   G. Allais
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   Guillaume Allais
• [Agda] Precedence of arrow   Guillaume Allais
• [Agda] a tutorial for proof by coinduction   Guillaume Allais
• [Agda] tracing & profiling   Guillaume Allais
• [Agda] How can I implement naive sized lambdas?   Guillaume Allais
• [Agda] splitting cases   Guillaume Allais
• [Agda] Compiling HelloWorld   Guillaume Allais
• [Agda] words   Guillaume Allais
• [Agda] Question about colists, musical notation vs coinductive records, and all that   Guillaume Allais
• [Agda] why is this corecursion red? And indexed coinductive definitions.   Guillaume Allais
• [Agda] status of inlining agda code   Thorsten Altenkirch
• [Agda] status of inlining agda code   Thorsten Altenkirch
• [Agda] agda latex mode   Thorsten Altenkirch
• [Agda] let vs where   Thorsten Altenkirch
• [Agda] let vs where   Thorsten Altenkirch
• [Agda] why coinductive?   Thorsten Altenkirch
• [Agda] why coinductive?   Thorsten Altenkirch
• [Agda] why coinductive?   Thorsten Altenkirch
• [Agda] [Coq-Club] Why dependent type theory?   Thorsten Altenkirch
• [Agda] [Coq-Club] Why dependent type theory?   Thorsten Altenkirch
• [Agda] [Coq-Club] Why dependent type theory?   Thorsten Altenkirch
• [Agda] [Coq-Club] Why dependent type theory? (resend)   Thorsten Altenkirch
• [Agda] [Coq-Club] Why dependent type theory?   Thorsten Altenkirch
• [Agda] [Coq-Club] Why dependent type theory?   Thorsten Altenkirch
• [Agda] [Coq-Club] Why dependent type theory?   Thorsten Altenkirch
• [Agda] what is happening here?   Thorsten Altenkirch
• [Agda] what is happening here?   Thorsten Altenkirch
• [Agda] Type Theory vs. Set Theory – Re: [Coq-Club] Why dependent type theory?   Thorsten Altenkirch
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   Thorsten Altenkirch
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   Thorsten Altenkirch
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   Thorsten Altenkirch
• [Agda] [Coq-Club] Concepts within Type Theory – Re: Type Theory vs. Set Theory – Re: Why dependent type theory?   Thorsten Altenkirch
• [Agda] Concepts within Type Theory – Re: [Coq-Club] Type Theory vs. Set Theory – Re: Why dependent type theory?   Thorsten Altenkirch
• [Agda] [Coq-Club] Concepts within Type Theory – Re: Type Theory vs. Set Theory – Re: Why dependent type theory?   Thorsten Altenkirch
• [Agda] [Coq-Club] Concepts within Type Theory – Re: Type Theory vs. Set Theory – Re: Why dependent type theory?   Thorsten Altenkirch
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   Thorsten Altenkirch
• [Agda] splitting cases   Thorsten Altenkirch
• [Agda] Induction from Sigma?   Thorsten Altenkirch
• [Agda] Example of an online conference in theoretical computer science BCTCS starting now   Thorsten Altenkirch
• [Agda] Automatic conversion between records and iterated Sigma types   Thorsten Altenkirch
• [Agda] Automatic conversion between records and iterated Sigma types   Thorsten Altenkirch
• [Agda] Strict equality _≣_ in agda   Thorsten Altenkirch
• [Agda] Strict equality _≣_ in agda   Thorsten Altenkirch
• [Agda] What do you use for variable binding in 2020?   Thorsten Altenkirch
• [Agda] why is this corecursion red? And indexed coinductive definitions.   Thorsten Altenkirch
• [Agda] installation trouble WAS Re: why is this corecursion red? And indexed coinductive definitions.   Thorsten Altenkirch
• [Agda] installation trouble WAS Re: why is this corecursion red? And indexed coinductive definitions.   Thorsten Altenkirch
• [Agda] why is this corecursion red? And indexed coinductive definitions.   Thorsten Altenkirch
• [Agda] how to evaluate in the current context   Thorsten Altenkirch
• [Agda] with + Path   Thorsten Altenkirch
• [Agda] how to evaluate in the current context   Thorsten Altenkirch
• [Agda] Understanding Glue   Thorsten Altenkirch
• [Agda] Understanding Glue   Thorsten Altenkirch
• [Agda] convertibility of implicit and explicit Pi-types   Thorsten Altenkirch
• [Agda] how do I quote agda code on the agda wiki?   Thorsten Altenkirch
• [Agda] A preliminary programme for AIM XXXII   Thorsten Altenkirch
• [Agda] AGDA XXXII has started   Thorsten Altenkirch
• [Agda] several agda versions   Thorsten Altenkirch
• [Agda] Moving Prop under Quantifiers?   Thorsten Altenkirch
• [Agda] Cabal hell again   Thorsten Altenkirch
• [Agda] Cabal hell again   Thorsten Altenkirch
• [Agda] Problem with generalised variables   Thorsten Altenkirch
• [Agda] Problem with generalised variables   Thorsten Altenkirch
• [Agda] Shadowing definitions   Thorsten Altenkirch
• [Agda] Shadowing definitions   Thorsten Altenkirch
• [Agda] Shadowing definitions   Thorsten Altenkirch
• [Agda] Weird termination problem   Thorsten Altenkirch
• [Agda] Weird termination problem   Thorsten Altenkirch
• [Agda] Weird termination problem   Thorsten Altenkirch
• [Agda] Weird termination problem   Thorsten Altenkirch
• [Agda] Hanging out with the Lean crowd   Thorsten Altenkirch
• [Agda] Question, re: x-dual-U exercise in Negation chapter of PLFA.   Thorsten Altenkirch
• [Agda] Overloaded constructor trouble   Thorsten Altenkirch
• [Agda] Overloaded constructor trouble   Thorsten Altenkirch
• [Agda] A philosophical question on absurd.   Thorsten Altenkirch
• [Agda] Fwd: Fwd: Question about transport and cubical   Thorsten Altenkirch
• [Agda] Converting intrinsically typed terms   Thorsten Altenkirch
• [Agda] Teaching positions at Nottingham   Thorsten Altenkirch
• [Agda] Tips for working around proof relevance   Thorsten Altenkirch
• [Agda] Tips for working around proof relevance   Thorsten Altenkirch
• [Agda] Tips for working around proof relevance   Thorsten Altenkirch
• [Agda] Tips for working around proof relevance   Thorsten Altenkirch
• [Agda] Tips for working around proof relevance   Thorsten Altenkirch
• [Agda] Tips for working around proof relevance   Thorsten Altenkirch
• [Agda] Tips for working around proof relevance   Thorsten Altenkirch
• [Agda] Tips for working around proof relevance   Thorsten Altenkirch
• [Agda] Agda Interactive Notebooks   Andrea Amantini
• [Agda] Agda Interactive Notebooks   Andrea Amantini
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Jesper Louis Andersen
• [Agda] Verifying type inference in Agda?   Kenichi Asai
• [Agda] Defining equality in Prop   Bob Atkey
• [Agda] Multiple Research Positions (3 Doctoral, 5 Post-doctoral) on AI Verification   Robert Atkey
• [Agda] [Coq-Club] Why dependent type theory?   Jeremy Avigad
• [Agda] [Coq-Club] Why dependent type theory?   Jeremy Avigad
• [Agda] [Coq-Club] Why dependent type theory?   Jeremy Avigad
• [Agda] TERMGRAPH 2020: Call for papers   Patrick Bahr
• [Agda] TERMGRAPH 2020: 2nd Call for papers   Patrick Bahr
• [Agda] TERMGRAPH 2020: Deadline Extension - 22 April   Patrick Bahr
• [Agda] TERMGRAPH 2020: Call for (Online) Participation   Patrick Bahr
• [Agda] [ANNOUNCE] Agda 2.6.1   Miëtek Bak
• [Agda] [ANNOUNCE] Agda 2.6.1   Miëtek Bak
• [Agda] Emacs mode setup command failing.   David Banas
• [Agda] Emacs mode setup command failing.   David Banas
• [Agda] List of fonts required for Emacs mode?   David Banas
• [Agda] List of fonts required for Emacs mode?   David Banas
• [Agda] List of fonts required for Emacs mode?   David Banas
• [Agda] rewrite construct not working, when Naturals defined locally?   David Banas
• [Agda] rewrite construct not working, when Naturals defined locally?   David Banas
• [Agda] Question, re: x-dual-U exercise in Negation chapter of PLFA.   David Banas
• [Agda] PLFA - Negation - Exercise Classical   David Banas
• [Agda] PLFA - Negation - Exercise Classical   David Banas
• [Agda] PLFA - Negation - Exercise Classical   David Banas
• [Agda] PLFA - Negation - Exercise Classical   David Banas
• [Agda] 2 tips for my fellow Agda newbies   David Banas
• [Agda] A philosophical question on absurd.   David Banas
• [Agda] A philosophical question on absurd.   David Banas
• [Agda] A philosophical question on absurd.   David Banas
• [Agda] Why the light gray highlighting here?   David Banas
• [Agda] Bit-wise XOR for Word64?   David Banas
• [Agda] Why are some terms in the Agda goal report colored blue?   David Banas
• [Agda] CMCS 2020: Final Call for Papers (extended deadlines)   Henning Basold
• [Agda] TEASE-LP (co-located with ETAPS 2020): Second call for contributions   Henning Basold
• [Agda] why coinductive?   Henning Basold
• [Agda] why coinductive?   Henning Basold
• [Agda] why coinductive?   Henning Basold
• [Agda] CMCS 2020: Call for Participation   Henning Basold
• [Agda] Hanging out with the Lean crowd   Henning Basold
• [Agda] 2nd Workshop on Formal Methods for Blockchains (FMBC) 2020 - 1st CFP   Bruno Bernardo
• [Agda] FMBC 2020: 2nd Workshop on Formal Methods for Blockchains (CfP, Deadline Extension)   Bruno Bernardo
• [Agda] FMBC 2020: 2nd Workshop on Formal Methods for Blockchains (3rd CfP, Deadline Extension)   Bruno Bernardo
• [Agda] FMBC 2020 - Call for Participation   Bruno Bernardo
• [Agda] Hanging out with the Lean crowd   Frédéric Blanqui
• [Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]   Frédéric Blanqui
• [Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]   Frédéric Blanqui
• [Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]   Frédéric Blanqui
• [Agda] slightly wrong sized datatype definition leads to proof of False   Frédéric Blanqui
• [Agda] slightly wrong sized datatype definition leads to proof of False   Frédéric Blanqui
• [Agda] Introducing Agdapad, a website for real-time collaborative Agda experiments (early preview)   Ingo Blechschmidt
• [Agda] how do I quote agda code on the agda wiki?   Ingo Blechschmidt
• [Agda] LSFA 2020 Second call for papers   Ana Bove
• [Agda] CFP: LSFA 2020   Ana Bove
• [Agda] LSFA 2020 - Deadline Extension   Ana Bove
• [Agda] Performance: opening parameterized modules before the fields of a record   Guillaume Brunerie
• [Agda] Performance: opening parameterized modules before the fields of a record   Guillaume Brunerie
• [Agda] Moving Prop under Quantifiers?   Guillaume Brunerie
• [Agda] Moving Prop under Quantifiers?   Guillaume Brunerie
• [Agda] Problem with generalised variables   Guillaume Brunerie
• [Agda] type-checking x=x   Guillaume Brunerie
• [Agda] Hanging out with the Lean crowd   Guillaume Brunerie
• [Agda] Hanging out with the Lean crowd   Guillaume Brunerie
• [Agda] Hanging out with the Lean crowd   Guillaume Brunerie
• [Agda] multiple instance resolution and negation   Guillaume Brunerie
• [Agda] Suspicious normalisation   Guillaume Brunerie
• [Agda] Suspicious normalisation   Guillaume Brunerie
• [Agda] Suspicious normalisation   Guillaume Brunerie
• [Agda] [Coq-Club] Why dependent type theory?   Kevin Buzzard
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   Kevin Buzzard
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   Kevin Buzzard
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Manuel Bärenz
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Manuel Bärenz
• [Agda] A philosophical question on absurd.   Manuel Bärenz
• [Agda] Question about transport and cubical   Manuel Bärenz
• [Agda] Fwd: Question about transport and cubical   Manuel Bärenz
• [Agda] Fwd: Fwd: Question about transport and cubical   Manuel Bärenz
• [Agda] Fwd: Fwd: Question about transport and cubical   Manuel Bärenz
• [Agda] Fwd: Fwd: Question about transport and cubical   Manuel Bärenz
• [Agda] Size Issue when Modelling Effectful Data Structures and Computations   Manuel Bärenz
• [Agda] nontermination and Sized types   Manuel Bärenz
• [Agda] slightly wrong sized datatype definition leads to proof of False   Manuel Bärenz
• [Agda] slightly wrong sized datatype definition leads to proof of False   Manuel Bärenz
• [Agda] slightly wrong sized datatype definition leads to proof of False   Manuel Bärenz
• [Agda] Formalization of a system dependently-typed records in Agda?   Jacques Carette
• [Agda] Automatic conversion between records and iterated Sigma types   Jacques Carette
• [Agda] Automatic conversion between records and iterated Sigma types   Jacques Carette
• [Agda] Automatic conversion between records and iterated Sigma types   Jacques Carette
• [Agda] Universe level in heterogeneous association list   Jacques Carette
• [Agda] problem with proj1   Jacques Carette
• [Agda] Performance: opening parameterized modules before the fields of a record   Jacques Carette
• [Agda] Cabal hell again   Carette, Jacques
• [Agda] Hanging out with the Lean crowd   Carette, Jacques
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Carette, Jacques
• [Agda] General notion of equality for syntactically equal objects with different types from the same datatype family?   Carette, Jacques
• [Agda] Tips for working around proof relevance   Carette, Jacques
• [Agda] agda-categories, a story   Carette, Jacques
• [Agda] Tips for working around proof relevance   Jacques Carette
• [Agda] irrelevancy annotation   Carette, Jacques
• [Agda] Info about instance resolution in macro   Joris Ceulemans
• [Agda] idiom brackets in 2.6.1   Liang-Ting Chen
• [Agda] Emacs mode setup command failing.   Liang-Ting Chen
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   David Thrane Christiansen
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   David Thrane Christiansen
• [Agda] How experimental is Cumulativity?   Jesper Cockx
• [Agda] How experimental is Cumulativity?   Jesper Cockx
• [Agda] PhD Position in in Theory and Implementation of Dependently Typed Programming Languages   Jesper Cockx
• [Agda] Coinductive records and separate files in Agda   Jesper Cockx
• [Agda] Unbound level variables in rewrite rule   Jesper Cockx
• [Agda] Rewrite rules for both Set and Prop   Jesper Cockx
• [Agda] Rewrite rules for both Set and Prop   Jesper Cockx
• [Agda] let vs where   Jesper Cockx
• [Agda] Fwd: [Coq-Club] Why dependent type theory?   Jesper Cockx
• [Agda] exercice of Peter Dybjer   Jesper Cockx
• [Agda] "Not in Scope" definitional equalities   Jesper Cockx
• [Agda] where is the official agda.sty   Jesper Cockx
• [Agda] error message in agda   Jesper Cockx
• [Agda] Automatic conversion between records and iterated Sigma types   Jesper Cockx
• [Agda] Automatic conversion between records and iterated Sigma types   Jesper Cockx
• [Agda] Automatic conversion between records and iterated Sigma types   Jesper Cockx
• [Agda] Automatic conversion between records and iterated Sigma types   Jesper Cockx
• [Agda] First-Class Type Issue   Jesper Cockx
• [Agda] An article by Jean-Yves Girard   Jesper Cockx
• [Agda] Strict equality _≣_ in agda   Jesper Cockx
• [Agda] --rewriting and the Agda standard library   Jesper Cockx
• [Agda] --rewriting and the Agda standard library   Jesper Cockx
• [Agda] Light grey background?   Jesper Cockx
• [Agda] Two assistant/associate professor positions in PL at TU Delft   Jesper Cockx
• [Agda] Termination Checking and WIthout-K   Jesper Cockx
• [Agda] Problem proving inequality with HeterogeneousEquality   Jesper Cockx
• [Agda] Problem proving inequality with HeterogeneousEquality   Jesper Cockx
• [Agda] Problem proving inequality with HeterogeneousEquality   Jesper Cockx
• [Agda] convertibility of implicit and explicit Pi-types   Jesper Cockx
• [Agda] type-checking x=x   Jesper Cockx
• [Agda] Hanging out with the Lean crowd   Jesper Cockx
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Jesper Cockx
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Jesper Cockx
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Jesper Cockx
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Jesper Cockx
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Jesper Cockx
• [Agda] Resolving a universe level problem   Jesper Cockx
• [Agda] Multi-line comments in literate Agda files   Jesper Cockx
• [Agda] Agda Implementors' Meeting XXXIII: Call for talks and participation   Jesper Cockx
• [Agda] Size Issue when Modelling Effectful Data Structures and Computations   Jesper Cockx
• [Agda] Question about inequality and absurd patterns   Jesper Cockx
• [Agda] Agda Implementors' Meeting XXXIII: Call for talks and participation   Jesper Cockx
• [Agda] Help with understanding REWRITE   Jesper Cockx
• [Agda] slightly wrong sized datatype definition leads to proof of False   Jesper Cockx
• [Agda] any known proof of ⊥ that does not syntactically use ∞ ?   Jesper Cockx
• [Agda] General notion of equality for syntactically equal objects with different types from the same datatype family?   Jesper Cockx
• [Agda] Inference difficulties   Jesper Cockx
• [Agda] Tips for working around proof relevance   Jesper Cockx
• [Agda] installing agda   Jesper Cockx
• [Agda] CFP: Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2020), with special session in honour of Frank Pfenning   Claudio Sacerdoti Coen
• [Agda] WFLP 2020 CFP (Workshop on Functional and Constraint Logic Programming)   Claudio Sacerdoti Coen
• [Agda] LFMTP2020 Call for Participation   Claudio Sacerdoti Coen
• [Agda] WFLP 2020: Deadline Extension   Claudio Sacerdoti Coen
• [Agda] WFLP 2020: Deadline Extension   Claudio Sacerdoti Coen
• [Agda] WFLP 2020: Deadline Extension   Claudio Sacerdoti Coen
• [Agda] LFMTP 2020 Post-Proceedings: Call for Papers   Claudio Sacerdoti Coen
• [Agda] Understanding Glue   Thierry Coquand
• [Agda] Installing standard and plfa libraries   Jonathan Steven Prieto Cubides
• [Agda] Termination checking with Lexicographic recursive calls   Matthew Daggitt
• [Agda] recursion, lexicographic ordering   Matthew Daggitt
• [Agda] recursion, lexicographic ordering   Matthew Daggitt
• [Agda] [ANNOUNCE] Agda 2.6.1   Matthew Daggitt
• [Agda] [ANNOUNCE] Standard library v1.3   Matthew Daggitt
• [Agda] --rewriting and the Agda standard library   Matthew Daggitt
• [Agda] many ways to import the same thing from record   Matthew Daggitt
• [Agda] [ANNOUNCE] Agda Standard Library 1.4 release candidate 1   Matthew Daggitt
• [Agda] [ANNOUNCE] Agda Standard Library 1.4 release candidate 1   Matthew Daggitt
• [Agda] [ANNOUNCE] Standard library v1.4   Matthew Daggitt
• [Agda] General notion of equality for syntactically equal objects with different types from the same datatype family?   Matthew Daggitt
• [Agda] General notion of equality for syntactically equal objects with different types from the same datatype family?   Matthew Daggitt
• [Agda] Isomorphisms, equational reasoning, and level changes   Matthew Daggitt
• [Agda] delaying computation to run time   Nils Anders Danielsson
• [Agda] delaying computation to run time   Nils Anders Danielsson
• [Agda] tracing & profiling   Nils Anders Danielsson
• [Agda] tracing & profiling   Nils Anders Danielsson
• [Agda] Struggling with irrelevance   Nils Anders Danielsson
• [Agda] type checking in real-world algebra   Nils Anders Danielsson
• [Agda] status of inlining agda code   Nils Anders Danielsson
• [Agda] status of inlining agda code   Nils Anders Danielsson
• [Agda] agda latex mode   Nils Anders Danielsson
• [Agda] Contributing: good first issues   Nils Anders Danielsson
• [Agda] Getting started: couple more questions   Nils Anders Danielsson
• [Agda] Termination checking with Lexicographic recursive calls   Nils Anders Danielsson
• [Agda] Termination checking with Lexicographic recursive calls   Nils Anders Danielsson
• [Agda] Agda Documentation   Nils Anders Danielsson
• [Agda] What to do when Rewrite fails?   Nils Anders Danielsson
• [Agda] what is happening here?   Nils Anders Danielsson
• [Agda] Example of an online conference in theoretical computer science BCTCS starting now   Nils Anders Danielsson
• [Agda] Installing standard and plfa libraries   Nils Anders Danielsson
• [Agda] StringOrInt function   Nils Anders Danielsson
• [Agda] Online Agda meeting?   Nils Anders Danielsson
• [Agda] Online Agda meeting?   Nils Anders Danielsson
• [Agda] --rewriting and the Agda standard library   Nils Anders Danielsson
• [Agda] Nat Fuel vs Sized Types (and other Sized Type questions)   Nils Anders Danielsson
• [Agda] Nat Fuel vs Sized Types (and other Sized Type questions)   Nils Anders Danielsson
• [Agda] Agda Implementors' Meeting XXXII   Nils Anders Danielsson
• [Agda] Light grey background?   Nils Anders Danielsson
• [Agda] lost in modules   Nils Anders Danielsson
• [Agda] installation trouble WAS Re: why is this corecursion red? And indexed coinductive definitions.   Nils Anders Danielsson
• [Agda] Question about colists, musical notation vs coinductive records, and all that   Nils Anders Danielsson
• [Agda] Data.Thunk, cofix question   Nils Anders Danielsson
• [Agda] "Failed to find source"   Nils Anders Danielsson
• [Agda] Data.Thunk, cofix question   Nils Anders Danielsson
• [Agda] how to evaluate in the current context   Nils Anders Danielsson
• [Agda] how to evaluate in the current context   Nils Anders Danielsson
• [Agda] A preliminary programme for AIM XXXII   Nils Anders Danielsson
• [Agda] Problem proving inequality with HeterogeneousEquality   Nils Anders Danielsson
• [Agda] installation problem   Nils Anders Danielsson
• [Agda] What does does it mean if "-invert730" shows up in a goal?   Nils Anders Danielsson
• [Agda] many ways to import the same thing from record   Nils Anders Danielsson
• [Agda] \ell does not display   Nils Anders Danielsson
• [Agda] Has Agda been tested on i686 architecture ?   Nils Anders Danielsson
• [Agda] \ell does not display   Nils Anders Danielsson
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Nils Anders Danielsson
• [Agda] Hanging out with the Lean crowd   Nils Anders Danielsson
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Nils Anders Danielsson
• [Agda] Hanging out with the Lean crowd   Nils Anders Danielsson
• [Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]   Nils Anders Danielsson
• [Agda] Multi-line comments in literate Agda files   Nils Anders Danielsson
• [Agda] Size Issue when Modelling Effectful Data Structures and Computations   Nils Anders Danielsson
• [Agda] Bit-wise XOR for Word64?   Nils Anders Danielsson
• [Agda] Why the light gray highlighting here?   Nils Anders Danielsson
• [Agda] nontermination and Sized types   Nils Anders Danielsson
• [Agda] nontermination and Sized types   Nils Anders Danielsson
• [Agda] slightly wrong sized datatype definition leads to proof of False   Nils Anders Danielsson
• [Agda] Negative coinductive sized types   Nils Anders Danielsson
• [Agda] Negative coinductive sized types   Nils Anders Danielsson
• [Agda] Online Agda meeting?   Mehmet Oguz Derin
• [Agda] Resolving a universe level problem   Marko Dimjašević
• [Agda] Resolving a universe level problem   Marko Dimjašević
• [Agda] Multi-line comments in literate Agda files   Marko Dimjašević
• [Agda] Multi-line comments in literate Agda files   Marko Dimjašević
• [Agda] Multi-line comments in literate Agda files   Marko Dimjašević
• [Agda] Suspicious normalisation   Marko Dimjašević
• [Agda] Suspicious normalisation   Marko Dimjašević
• [Agda] Suspicious normalisation   Marko Dimjašević
• [Agda] Cabal hell again   Dan Doel
• [Agda] Converting intrinsically typed terms   Conal Elliott
• [Agda] Converting intrinsically typed terms   Conal Elliott
• [Agda] Inference difficulties   Conal Elliott
• [Agda] Inference difficulties   Conal Elliott
• [Agda] Isomorphisms, equational reasoning, and level changes   Conal Elliott
• [Agda] Negative coinductive sized types   Florian Engel
• [Agda] Negative coinductive sized types   Florian Engel
• [Agda] Negative coinductive sized types   Florian Engel
• [Agda] How experimental is Cumulativity?   Joey Eremondi
• [Agda] What to do when Rewrite fails?   Joey Eremondi
• [Agda] Induction from Sigma?   Joey Eremondi
• [Agda] Induction from Sigma?   Joey Eremondi
• [Agda] Nat Fuel vs Sized Types (and other Sized Type questions)   Joey Eremondi
• [Agda] What do you use for variable binding in 2020?   Joey Eremondi
• [Agda] Nat Fuel vs Sized Types (and other Sized Type questions)   Joey Eremondi
• [Agda] Termination Checking and WIthout-K   Joey Eremondi
• [Agda] Value-recursive records?   Joey Eremondi
• [Agda] What does does it mean if "-invert730" shows up in a goal?   Joey Eremondi
• [Agda] Moving Prop under Quantifiers?   Joey Eremondi
• [Agda] Moving Prop under Quantifiers?   Joey Eremondi
• [Agda] Moving Prop under Quantifiers?   Joey Eremondi
• [Agda] Precedence of arrow   Martin Escardo
• [Agda] Why dependent type theory?   Martin Escardo
• [Agda] Why dependent type theory?   Martin Escardo
• [Agda] Why dependent type theory?   Martin Escardo
• [Agda] Why dependent type theory?   Martin Escardo
• [Agda] Concepts within Type Theory – Re: [Coq-Club] Type Theory vs. Set Theory – Re: Why dependent type theory?   Martin Escardo
• [Agda] syntax declaration   Martin Escardo
• [Agda] syntax declaration   Martin Escardo
• [Agda] Automatic conversion between records and iterated Sigma types   Martin Escardo
• [Agda] Automatic conversion between records and iterated Sigma types   Martin Escardo
• [Agda] Automatic conversion between records and iterated Sigma types   Martin Escardo
• [Agda] Automatic conversion between records and iterated Sigma types   Martin Escardo
• [Agda] An article by Jean-Yves Girard   Martin Escardo
• [Agda] An article by Jean-Yves Girard   Martin Escardo
• [Agda] Agda patterns   Martin Escardo
• [Agda] Agda patterns   Martin Escardo
• [Agda] Agda patterns   Martin Escardo
• [Agda] PhD Scholarships in Mathematics and computation   Martin Escardo
• [Agda] type-checking x=x   Martin Escardo
• [Agda] Hanging out with the Lean crowd   Martin Escardo
• [Agda] Hanging out with the Lean crowd   Martin Escardo
• [Agda] Hanging out with the Lean crowd   Martin Escardo
• [Agda] Hanging out with the Lean crowd   Martin Escardo
• [Agda] Hanging out with the Lean crowd   Martin Escardo
• [Agda] Hanging out with the Lean crowd   Martin Escardo
• [Agda] Agda on raspberry pi 4   Martin Escardo
• [Agda] Question about colists, musical notation vs coinductive records, and all that   Eric Finster
• [Agda] Question about colists, musical notation vs coinductive records, and all that   Eric Finster
• [Agda] Permanent positions at the University of Strathclyde   Fredrik Nordvall Forsberg
• [Agda] Suspicious normalisation   Fredrik Nordvall Forsberg
• [Agda] Hanging out with the Lean crowd   Louis Garde
• [Agda] How can I implement naive sized lambdas?   Dr. ERDI Gergo
• [Agda] Termination checking with Lexicographic recursive calls   Sergey Goncharov
• [Agda] Termination checking with Lexicographic recursive calls   Sergey Goncharov
• [Agda] Termination checking with Lexicographic recursive calls   Sergey Goncharov
• [Agda] Termination checking with Lexicographic recursive calls   Sergey Goncharov
• [Agda] "Not in Scope" definitional equalities   Sergey Goncharov
• [Agda] [lean-user] Why dependent type theory?   Colin Stebbins Gordon
• [Agda] Why dependent type theory?   Jason Gross
• [Agda] [Coq-Club] Why dependent type theory?   Jason Gross
• [Agda] [Coq-Club] Why dependent type theory?   Jason Gross
• [Agda] Prior work on proof assistant performance / optimization   Jason Gross
• [Agda] Prior work on proof assistant performance / optimization   Jason Gross
• [Agda] First call for draft papers for IFL 2020 (Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] Second call for draft papers for IFL 2020 (Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] Third call for draft papers for IFL 2020 (Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] First and Only Call for Participation for IFL 2020 (Implementation and Application of Functional Languages)   Jurriaan Hage
• [Agda] An article by Jean-Yves Girard   Peter Hancock
• [Agda] Hanging out with the Lean crowd   Peter Hancock
• [Agda] A philosophical question on absurd.   Peter Hancock
• [Agda] Agda on raspberry pi 4   Peter Hancock
• [Agda] Coinductive records and separate files in Agda   William Harrison
• [Agda] Question about colists, musical notation vs coinductive records, and all that   William Harrison
• [Agda] Question about colists, musical notation vs coinductive records, and all that   William Harrison
• [Agda] Question about colists, musical notation vs coinductive records, and all that   William Harrison
• [Agda] Data.Thunk, cofix question   William Harrison
• [Agda] Data.Thunk, cofix question   William Harrison
• [Agda] Weird termination problem   William Harrison
• [Agda] Verifying type inference in Agda?   William Harrison
• [Agda] Question about inequality and absurd patterns   William Harrison
• [Agda] Converting intrinsically typed terms   William Harrison
• [Agda] Getting started: Emacs   Jason -Zhong Sheng- Hu
• [Agda] recursion, lexicographic ordering   Jason -Zhong Sheng- Hu
• [Agda] add to the Agda group on Github   Jason -Zhong Sheng- Hu
• [Agda] syntax declaration   Jason -Zhong Sheng- Hu
• [Agda] error in plfa exercise   Jason -Zhong Sheng- Hu
• [Agda] What do you use for variable binding in 2020?   Jason -Zhong Sheng- Hu
• [Agda] Weird termination problem   Jason -Zhong Sheng- Hu
• [Agda] Weird termination problem   Jason -Zhong Sheng- Hu
• [Agda] Why the light gray highlighting here?   Jason -Zhong Sheng- Hu
• [Agda] Why the light gray highlighting here?   Jason -Zhong Sheng- Hu
• [Agda] 10 PhD studentships in Nottingham for Home/EU applicants   Graham Hutton
• [Agda] Journal of Functional Programming - Call for PhD Abstracts   Graham Hutton
• [Agda] Journal of Functional Programming - Call for PhD Abstracts   Graham Hutton
• [Agda] Three new Teaching Assistant positions in Nottingham   Graham Hutton
• [Agda] Converting intrinsically typed terms   Harley D. Eades III
• [Agda] How can I implement naive sized lambdas?   Tom Jack
• [Agda] Problem proving inequality with HeterogeneousEquality   Tom Jack
• [Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]   Víctor López Juan
• [Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]   Víctor López Juan
• [Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]   Víctor López Juan
• [Agda] [Coq-Club] Why dependent type theory?   Ralf Jung
• [Agda] [Coq-Club] Prior work on proof assistant performance / optimization   Wolfram Kahl
• [Agda] Agda Documentation   Panos Ked
• [Agda] Problem proving inequality with HeterogeneousEquality   Donnacha Oisín Kidney
• [Agda] PhD studentships in Robotics (Edinburgh Center for Robotics)   Ekaterina Komendantskaya
• [Agda] How can I implement naive sized lambdas?   András Kovács
• [Agda] Prior work on proof assistant performance / optimization   András Kovács
• [Agda] [Coq-Club] Prior work on proof assistant performance / optimization   András Kovács
• [Agda] Defining equality in Prop   András Kovács
• [Agda] List of fonts required for Emacs mode?   András Kovács
• [Agda] List of fonts required for Emacs mode?   András Kovács
• [Agda] Hanging out with the Lean crowd   András Kovács
• [Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]   András Kovács
• [Agda] General notion of equality for syntactically equal objects with different types from the same datatype family?   András Kovács
• [Agda] Moving Prop under Quantifiers?   Nicolai Kraus
• [Agda] Hanging out with the Lean crowd   Nicolai Kraus
• [Agda] Hanging out with the Lean crowd   Nicolai Kraus
• [Agda] Hanging out with the Lean crowd   Nicolai Kraus
• [Agda] PLFA - Negation - Exercise Classical   Nicolai Kraus
• [Agda] Tips for working around proof relevance   Nicolai Kraus
• [Agda] Tips for working around proof relevance   Nicolai Kraus
• [Agda] Tips for working around proof relevance   Nicolai Kraus
• [Agda] Tips for working around proof relevance   Nicolai Kraus
• [Agda] Tips for working around proof relevance   Nicolai Kraus
• [Agda] Tips for working around proof relevance   Nicolai Kraus
• [Agda] Fwd: Fwd: Question about transport and cubical   Dan Krejsa
• [Agda] Fwd: Fwd: Question about transport and cubical   Dan Krejsa
• [Agda] An article by Jean-Yves Girard   Neel Krishnaswami
• [Agda] Hanging out with the Lean crowd   Neel Krishnaswami
• [Agda] Help with stuck unification/intrinsic typing in general   Neel Krishnaswami
• [Agda] Why dependent type theory?   Ken Kubota
• [Agda] Type Theory vs. Set Theory – Re: [Coq-Club] Why dependent type theory?   Ken Kubota
• [Agda] Concepts within Type Theory – Re: [Coq-Club] Type Theory vs. Set Theory – Re: Why dependent type theory?   Ken Kubota
• [Agda] [Coq-Club] Concepts within Type Theory – Re: Type Theory vs. Set Theory – Re: Why dependent type theory?   Ken Kubota
• [Agda] [Coq-Club] Concepts within Type Theory – Re: Type Theory vs. Set Theory – Re: Why dependent type theory?   Ken Kubota
• [Agda] Struggling with irrelevance   Mathijs Kwik
• [Agda] Struggling with irrelevance   Mathijs Kwik
• [Agda] Struggling with irrelevance   Mathijs Kwik
• [Agda] [2.6.1] erasure and irrelevance unpredictable   Mathijs Kwik
• [Agda] Online Agda meeting?   Andreas Källberg
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Andreas Källberg
• [Agda] Question about transport and cubical   Andreas Källberg
• [Agda] Shadowing definitions   Larrytheliquid
• [Agda] Shadowing definitions   Larrytheliquid
• [Agda] Help with stuck unification/intrinsic typing in general   Daniel Lee
• [Agda] Tips for working around proof relevance   Daniel Lee
• [Agda] Tips for working around proof relevance   Daniel Lee
• [Agda] Tips for working around proof relevance   Daniel Lee
• [Agda] Why is this non-terminating?   Jinwoo Lee
• [Agda] Why is this non-terminating?   Jinwoo Lee
• [Agda] Why is this non-terminating?   Jinwoo Lee
• [Agda] unfolding just a single definition in the context of a goal   Marcus Christian Lehmann
• [Agda] unfolding just a single definition in the context of a goal   Marcus Christian Lehmann
• [Agda] multiple instance resolution and negation   Marcus Christian Lehmann
• [Agda] multiple instance resolution and negation   Marcus Christian Lehmann
• [Agda] multiple instance resolution and negation   Marcus Christian Lehmann
• [Agda] splitting cases   John Leo
• [Agda] Online Agda meeting?   John Leo
• [Agda] Question about transport and cubical   John Leo
• [Agda] Fwd: Question about transport and cubical   John Leo
• [Agda] Fwd: Fwd: Question about transport and cubical   John Leo
• [Agda] Fwd: Fwd: Question about transport and cubical   John Leo
• [Agda] Fwd: Fwd: Question about transport and cubical   John Leo
• [Agda] Fwd: Fwd: Question about transport and cubical   John Leo
• [Agda] install agda   Pierre Lescanne
• [Agda] Strange bug   Pierre Lescanne
• [Agda] \ell does not display   Pierre Lescanne
• [Agda] package agda-mode not working   Michel Levy
• [Agda] failure of cabal install Agda   Michel Levy
• [Agda] failure of cabal install Agda   Michel Levy
• [Agda] failure of cabal install Agda   Michel Levy
• [Agda] failure of cabal install Agda   Michel Levy
• [Agda] exercice of Peter Dybjer   Michel Levy
• [Agda] where is the official agda.sty   Michel Levy
• [Agda] syntax declaration   Michel Levy
• [Agda] syntax declaration   Michel Levy
• [Agda] syntax declaration   Michel Levy
• [Agda] error message in agda   Michel Levy
• [Agda] rewrite keyword   Michel Levy
• [Agda] Installing standard and plfa libraries   Michel Levy
• [Agda] Installing standard and plfa libraries   Michel Levy
• [Agda] error in plfa exercise   Michel Levy
• [Agda] error in plfa exercise   Michel Levy
• [Agda] error in plfa exercise   Michel Levy
• [Agda] plfa, using proj2, missing in Quantifiers   Michel Levy
• [Agda] problem with proj1   Michel Levy
• [Agda] lost in modules   Michel Levy
• [Agda] lost in modules   Michel Levy
• [Agda] install agda   Michel Levy
• [Agda] install agda   Michel Levy
• [Agda] install agda   Michel Levy
• [Agda] install agda   Michel Levy
• [Agda] install agda   Michel Levy
• [Agda] lost in modules   Michel Levy
• [Agda] problem with install Agda   Michel Levy
• [Agda] installation problem   Michel Levy
• [Agda] installation problem   Michel Levy
• [Agda] Why the light gray highlighting here?   Thomas Lopatic
• [Agda] Why the light gray highlighting here?   Thomas Lopatic
• [Agda] Tips for working around proof relevance   Peter LeFanu Lumsdaine
• [Agda] idiom brackets in 2.6.1   Georgi Lyubenov
• [Agda] How can I implement naive sized lambdas?   Georgi Lyubenov
• [Agda] rewrite keyword   Georgi Lyubenov
• [Agda] How can I implement naive sized lambdas?   Georgi Lyubenov
• [Agda] Online Agda meeting?   Georgi Lyubenov
• [Agda] Cabal hell again   Georgi Lyubenov
• [Agda] rewrite construct not working, when Naturals defined locally?   Georgi Lyubenov
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Georgi Lyubenov
• [Agda] Why the light gray highlighting here?   Georgi Lyubenov
• [Agda] when to set underscore suffix?   Georgi Lyubenov
• [Agda] when to set underscore suffix?   Georgi Lyubenov
• [Agda] Agda and machine learning   Warrick Macmillan
• [Agda] Why dependent type theory?   James McKinna
• [Agda] Why dependent type theory?   James McKinna
• [Agda] Weird instance propagation between parameterised modules   Orestis Melkonian
• [Agda] Weird instance propagation between parameterised modules   Orestis Melkonian
• [Agda] [Coq-Club] [lean-user] Re: Why dependent type theory?   Stefan Monnier
• [Agda] [Coq-Club] Prior work on proof assistant performance / optimization   Stefan Monnier
• [Agda] [lean-user] Why dependent type theory?   Scott Morrison
• [Agda] PhD positions in Computational Mathematics at Stockholm University   Anders Mortberg
• [Agda] Automatic conversion between records and iterated Sigma types   Anders Mortberg
• [Agda] Online Agda meeting?   Anders Mortberg
• [Agda] Fwd: Fwd: Question about transport and cubical   Anders Mortberg
• [Agda] Fwd: Fwd: Question about transport and cubical   Anders Mortberg
• [Agda] Fwd: Fwd: Question about transport and cubical   Anders Mortberg
• [Agda] Tips for working around proof relevance   Anders Mortberg
• [Agda] Tips for working around proof relevance   Anders Mortberg
• [Agda] Example of an online conference in theoretical computer science BCTCS starting now   Shin-Cheng Mu
• [Agda] Problem proving inequality with HeterogeneousEquality   Shin-Cheng Mu
• [Agda] Online Agda meeting?   Alexander Ben Nasrallah
• [Agda] _≡⟨_⟩_ operator   Alexander Ben Nasrallah
• [Agda] Using Haskell type class constraints with Agda types   Alexander Ben Nasrallah
• [Agda] Using Haskell type class constraints with Agda types   Alexander Ben Nasrallah
• [Agda] MSFP 2020 - Final Call for Papers   Max New
• [Agda] MSFP 2020 (Monday August 31st and Tuesday September 1st) - Call for Participation   Max New
• [Agda] tracing & profiling   Ulf Norell
• [Agda] Struggling with irrelevance   Ulf Norell
• [Agda] Struggling with irrelevance   Ulf Norell
• [Agda] [Coq-Club] Why dependent type theory?   Ulf Norell
• [Agda] add to the Agda group on Github   Ulf Norell
• [Agda] what is happening here?   Ulf Norell
• [Agda] syntax declaration   Ulf Norell
• [Agda] First-Class Type Issue   Ulf Norell
• [Agda] bottom and false   Ulf Norell
• [Agda] Agda patterns   Ulf Norell
• [Agda] Agda patterns   Ulf Norell
• [Agda] Overloaded constructor trouble   Ulf Norell
• [Agda] [ANNOUNCE] Agda 2.6.1.1   Ulf Norell
• [Agda] Info about instance resolution in macro   Ulf Norell
• [Agda] Using Haskell type class constraints with Agda types   Ulf Norell
• [Agda] Weird instance propagation between parameterised modules   Ulf Norell
• [Agda] irrelevancy annotation   Ulf Norell
• [Agda] Agda on Github Pages   Ed Nutting
• [Agda] Introducing hypotheses   Andreas Nuyts
• [Agda] Light grey background?   Andreas Nuyts
• [Agda] Understanding Glue   Andreas Nuyts
• [Agda] Call for Papers: APLAS 2020   Bruno Oliveira
• [Agda] Final Call for Papers: APLAS 2020 (deadline on the 6th of July)   Bruno Oliveira
• [Agda] APLAS 2020 Call for Participation   Bruno Oliveira
• [Agda] Milestone-Based Paid Remote Short-Term Projects in Formalization of Algorithms   Mateus de Oliveira Oliveira
• [Agda] TyDe 2020 - Final Call for Papers   Cyrus Omar
• [Agda] Universe level in heterogeneous association list   Nicolas Osborne
• [Agda] Universe level in heterogeneous association list   Nicolas Osborne
• [Agda] [Coq-Club] Why dependent type theory?   Miguel Pagano
• [Agda] [ANNOUNCE] Agda 2.6.1   Herminie Pagel
• [Agda] [ANNOUNCE] Agda 2.6.1   Herminie Pagel
• [Agda] Example of an online conference in theoretical computer science BCTCS starting now   Herminie Pagel
• [Agda] Example of an online conference in theoretical computer science BCTCS starting now   Herminie Pagel
• [Agda] Compiling HelloWorld   Herminie Pagel
• [Agda] Strict equality _≣_ in agda   Herminie Pagel
• [Agda] Strict equality _≣_ in agda   Herminie Pagel
• [Agda] F-IDE 2021 - Call for Papers   Andrei Paskevich
• [Agda] consistency   Patricia Peratto
• [Agda] consistency   Patricia Peratto
• [Agda] [Coq-Club] Why dependent type theory?   Patricia Peratto
• [Agda] bottom and false   Patricia Peratto
• [Agda] installing agda   Patricia Peratto
• [Agda] Nat Fuel vs Sized Types (and other Sized Type questions)   Andrew M. Pitts
• [Agda] Nat Fuel vs Sized Types (and other Sized Type questions)   Andrew M. Pitts
• [Agda] Defining equality in Prop   Andrew M. Pitts
• [Agda] nontermination and Sized types   Andrew M. Pitts
• [Agda] Help with understanding REWRITE   Andrew M. Pitts
• [Agda] Help with understanding REWRITE   Andrew M. Pitts
• [Agda] Certified Programs and Proofs (CPP) 2021: First Call for Papers   Andrei Popescu
• [Agda] Certified Programs and Proofs (CPP) 2021: Final Call for Papers   Andrei Popescu
• [Agda] CPP 2021 abstract deadline due soon (in ~23 hours)   Andrei Popescu
• [Agda] two proof-assistant friendly posts of Lecturer in Cybersecurity at University of Sheffield: deadline 3rd December 2020   Andrei Popescu
• [Agda] fully funded PhD position at University of Sheffield on the formal verification of industrial robots   Andrei Popescu
• [Agda] CPP 2021: Call for Participation and Lightning Talks   Andrei Popescu
• [Agda] A philosophical question on absurd.   Nicolas Pouillard
• [Agda] [Coq-Club] Why dependent type theory?   Pierre-Marie Pédrot
• [Agda] [Coq-Club] Why dependent type theory?   Pierre-Marie Pédrot
• [Agda] An article by Jean-Yves Girard   Xuanrui Qi
• [Agda] Induction from Sigma?   Jakob von Raumer
• [Agda] Light grey background?   Jakob von Raumer
• [Agda] Light grey background?   Jakob von Raumer
• [Agda] L and inverted L characters   Philippe de Rochambeau
• [Agda] L and inverted L characters   Philippe de Rochambeau
• [Agda] L and inverted L characters   Philippe de Rochambeau
• [Agda] Compiling HelloWorld   Philippe de Rochambeau
• [Agda] Compiling HelloWorld   Philippe de Rochambeau
• [Agda] StringOrInt function   Philippe de Rochambeau
• [Agda] Compiling HelloWorld   Philippe de Rochambeau
• [Agda] First-Class Type Issue   Philippe de Rochambeau
• [Agda] Online Agda meeting?   Philippe de Rochambeau
• [Agda] words   Philippe de Rochambeau
• [Agda] Introducing hypotheses   Philippe de Rochambeau
• [Agda] Introducing hypotheses   Philippe de Rochambeau
• [Agda] Introducing hypotheses   Philippe de Rochambeau
• [Agda] An article by Jean-Yves Girard   Philippe de Rochambeau
• [Agda] An article by Jean-Yves Girard   Philippe de Rochambeau
• [Agda] An article by Jean-Yves Girard   Philippe de Rochambeau
• [Agda] An article by Jean-Yves Girard   Philippe de Rochambeau
• [Agda] An article by Jean-Yves Girard   Philippe de Rochambeau
• [Agda] Boolean And in Pair   Philippe de Rochambeau
• [Agda] Boolean And in Pair   Philippe de Rochambeau
• [Agda] Boolean And in Pair   Philippe de Rochambeau
• [Agda] Boolean And in Pair   Philippe de Rochambeau
• [Agda] _≡⟨_⟩_ operator   Philippe de Rochambeau
• [Agda] _≡⟨_⟩_ operator   Philippe de Rochambeau
• [Agda] what is happening here?   Roman
• [Agda] Automatic conversion between records and iterated Sigma types   Roman
• [Agda] Automatic conversion between records and iterated Sigma types   Roman
• [Agda] Problem proving inequality with HeterogeneousEquality   Roman
• [Agda] Multi-line comments in literate Agda files   Roman
• [Agda] A tutorial on inference in Agda   Roman
• [Agda] slightly wrong sized datatype definition leads to proof of False   Vlad Rusu
• [Agda] slightly wrong sized datatype definition leads to proof of False   Vlad Rusu
• [Agda] any known proof of ⊥ that does not syntactically use ∞ ?   Vlad Rusu
• [Agda] Hanging out with the Lean crowd   Jorge Blázquez Saborido
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   Jorge Blázquez Saborido
• [Agda] Defining equality in Prop   Christian Sattler
• [Agda] Why dependent type theory?   Gabriel Scherer
• [Agda] Unbound level variables in rewrite rule   Filippo Sestini
• [Agda] Unbound level variables in rewrite rule   Filippo Sestini
• [Agda] Rewrite rules for both Set and Prop   Filippo Sestini
• [Agda] Why dependent type theory?   Steven Shaw
• [Agda] Why dependent type theory?   Steven Shaw
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 2   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 2   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 2   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.6.1   Andrés Sicard-Ramírez
• [Agda] [ANNOUNCE] Agda 2.6.1   Andrés Sicard-Ramírez
• [Agda] failure of cabal install Agda   Andrés Sicard-Ramírez
• [Agda] failure of cabal install Agda   Andrés Sicard-Ramírez
• [Agda] error in plfa exercise   Andrés Sicard-Ramírez
• [Agda] failure of cabal install Agda   Andrés Sicard-Ramírez
• [Agda] install agda   Andrés Sicard-Ramírez
• [Agda] install agda   Andrés Sicard-Ramírez
• [Agda] install agda   Andrés Sicard-Ramírez
• [Agda] install agda   Andrés Sicard-Ramírez
• [Agda] problem with install Agda   Andrés Sicard-Ramírez
• [Agda] recursion, lexicographic ordering   Siek, Jeremy
• [Agda] recursion, lexicographic ordering   Siek, Jeremy
• [Agda] --rewriting and the Agda standard library   Siek, Jeremy
• [Agda] --rewriting and the Agda standard library   Siek, Jeremy
• [Agda] --rewriting and the Agda standard library   Siek, Jeremy
• [Agda] What do you use for variable binding in 2020?   Siek, Jeremy
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   Bas Spitters
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   Bas Spitters
• [Agda] Automatic conversion between records and iterated Sigma types   Bas Spitters
• [Agda] Automatic conversion between records and iterated Sigma types   Bas Spitters
• [Agda] How experimental is Cumulativity?   Jon Sterling
• [Agda] How experimental is Cumulativity?   Jon Sterling
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   Jon Sterling
• [Agda] How can I implement naive sized lambdas?   Sandro Stucki
• [Agda] A philosophical question on absurd.   Sandro Stucki
• [Agda] forced arguments in EqReasoning   Sandro Stucki
• [Agda] forced arguments in EqReasoning   Sandro Stucki
• [Agda] Tips for working around proof relevance   Sandro Stucki
• [Agda] free download of VFPIA   Aaron Stump
• [Agda] Converting intrinsically typed terms   Aaron Stump
• [Agda] agda-categories, a story   Aaron Stump
• [Agda] Converting intrinsically typed terms   Swierstra, W.S. (Wouter)
• [Agda] Two PhD positions in Utrecht   Wouter Swierstra
• [Agda] Shadowing definitions   Peter Thiemann
• [Agda] Overloaded constructor trouble   Peter Thiemann
• [Agda] Verifying type inference in Agda?   Peter Thiemann
• [Agda] Call for Papers: PACMPL issue ICFP 2020   Sam Tobin-Hochstadt
• [Agda] ICFP 2020 will be held ONLINE Aug 23-28   Sam Tobin-Hochstadt
• [Agda] Call for Submissions: ICFP Student Research Competition   Sam Tobin-Hochstadt
• [Agda] Call for Tutorial Proposals: ICFP 2020   Sam Tobin-Hochstadt
• [Agda] Call for Participation: ICFP 2020   Sam Tobin-Hochstadt
• [Agda] Final Call for Tutorials, Discussions, and Social Events: ICFP 2020   Sam Tobin-Hochstadt
• [Agda] Second Call for Participation: ICFP 2020   Sam Tobin-Hochstadt
• [Agda] Call for Tutorial Participation: ICFP 2020   Sam Tobin-Hochstadt
• [Agda] Third Call for Participation: ICFP 2020   Sam Tobin-Hochstadt
• [Agda] Call for Workshop Proposals: ICFP 2021   Sam Tobin-Hochstadt
• [Agda] Rewriting rules in parametrized modules   Andrej Tokarčík
• [Agda] [Coq-Club] Why dependent type theory?   Dominique Unruh
• [Agda] [Coq-Club] Why dependent type theory?   Josef Urban
• [Agda] ETAPS Test of Time Award 2020, call for nominations   Tarmo Uustalu
• [Agda] First ETAPS Doctoral Dissertation Award, final call for nominations   Tarmo Uustalu
• [Agda] ETAPS 2020 afternoon, online, 2 July 2020, call for participation   Tarmo Uustalu
• [Agda] ETAPS 2021 1st joint call for papers   Tarmo Uustalu
• [Agda] ETAPS 2021 2nd joint call for papers   Tarmo Uustalu
• [Agda] ETAPS 2021 final joint call for papers   Tarmo Uustalu
• [Agda] Getting started: Emacs   Vox Veritatis
• [Agda] Getting started: couple more questions   Vox Veritatis
• [Agda] slightly wrong sized datatype definition leads to proof of False   Andrea Vezzosi
• [Agda] slightly wrong sized datatype definition leads to proof of False   Andrea Vezzosi
• [Agda] nontermination and Sized types   Vlad
• [Agda] Getting started: Emacs   Philip Wadler
• [Agda] syntax declaration   Philip Wadler
• [Agda] rewrite keyword   Philip Wadler
• [Agda] How can I implement naive sized lambdas?   Philip Wadler
• [Agda] Installing standard and plfa libraries   Philip Wadler
• [Agda] error in plfa exercise   Philip Wadler
• [Agda] plfa, using proj2, missing in Quantifiers   Philip Wadler
• [Agda] An article by Jean-Yves Girard   Philip Wadler
• [Agda] Light grey background?   Philip Wadler
• [Agda] Boolean And in Pair   Philip Wadler
• [Agda] _≡⟨_⟩_ operator   Philip Wadler
• [Agda] Shadowing definitions   Philip Wadler
• [Agda] PLFA - Negation - Exercise Classical   Philip Wadler
• [Agda] Why the light gray highlighting here?   Philip Wadler
• [Agda] Verifying type inference in Agda?   Philip Wadler
• [Agda] ML Family Workshop 2020: Call for presentations   Leo White
• [Agda] ML Family Workshop 2020: Deadline extension   Leo White
• [Agda] equality on Char   James Wood
• [Agda] consistency   James Wood
• [Agda] idiom brackets in 2.6.1   James Wood
• [Agda] exercice of Peter Dybjer   James Wood
• [Agda] Filling squares   James Wood
• [Agda] StringOrInt function   James Wood
• [Agda] Compiling HelloWorld   James Wood
• [Agda] Compiling HelloWorld   James Wood
• [Agda] Strict equality _≣_ in agda   James Wood
• [Agda] What do you use for variable binding in 2020?   James Wood
• [Agda] a strange function type report   James Wood
• [Agda] Question about colists, musical notation vs coinductive records, and all that   James Wood
• [Agda] Boolean And in Pair   James Wood
• [Agda] how to evaluate in the current context   James Wood
• [Agda] how do I quote agda code on the agda wiki?   James Wood
• [Agda] many ways to import the same thing from record   James Wood
• [Agda] many ways to import the same thing from record   James Wood
• [Agda] Why is this non-terminating?   James Wood
• [Agda] Why is this non-terminating?   James Wood
• [Agda] unfolding just a single definition in the context of a goal   James Wood
• [Agda] type-checking x=x   James Wood
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   James Wood
• [Agda] Hanging out with the Lean crowd   James Wood
• [Agda] Hanging out with the Lean crowd   James Wood
• [Agda] Question, re: x-dual-U exercise in Negation chapter of PLFA.   James Wood
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   James Wood
• [Agda] nontermination and Sized types   James Wood
• [Agda] a strange "unsolved" report   James Wood
• [Agda] a strange "unsolved" report   James Wood
• [Agda] a strange "unsolved" report   James Wood
• [Agda] a strange "unsolved" report   James Wood
• [Agda] when to set underscore suffix?   James Wood
• [Agda] forced arguments in EqReasoning   James Wood
• [Agda] forced arguments in EqReasoning   James Wood
• [Agda] Tips for working around proof relevance   James Wood
• [Agda] installing agda   James Wood
• [Agda] Tips for working around proof relevance   James Wood
• [Agda] When I try to reduce, I get a meta. (Reflection).   Apostolis Xekoukoulotakis
• [Agda] When I try to reduce, I get a meta. (Reflection).   Apostolis Xekoukoulotakis
• [Agda] syntax declaration   a.j.rouvoet
• [Agda] rewrite keyword   a.j.rouvoet
• [Agda] L and inverted L characters   a.j.rouvoet
• [Agda] L and inverted L characters   a.j.rouvoet
• [Agda] Online Agda meeting?   a.j.rouvoet
• [Agda] Boolean And in Pair   a.j.rouvoet
• [Agda] Cabal hell again   a.j.rouvoet
• [Agda] problem with algebraic hierarchy   a.j.rouvoet
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   a.j.rouvoet
• [Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)   a.j.rouvoet
• [Agda] Help with stuck unification/intrinsic typing in general   guillaume allais
• [Agda] nontermination and Sized types   guillaume allais
• [Agda] forced arguments in EqReasoning   guillaume allais
• [Agda] CfP for TYPES 2020 postproceedings:   Ugo de'Liguoro
• [Agda] StringOrInt function   phiroc at free.fr
• [Agda] StringOrInt function   phiroc at free.fr
• [Agda] Compiling HelloWorld   phiroc at free.fr
• [Agda] An article by Jean-Yves Girard   phiroc at free.fr
• [Agda] Transcendental Syntax   phiroc at free.fr
• [Agda] An article by Jean-Yves Girard   phiroc at free.fr
• [Agda] Getting started: Emacs   william.lawrence.harrison at gmail.com
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1   mechvel at scico.botik.ru
• [Agda] delaying computation to run time   mechvel at scico.botik.ru
• [Agda] delaying computation to run time   mechvel at scico.botik.ru
• [Agda] tracing & profiling   mechvel at scico.botik.ru
• [Agda] tracing & profiling   mechvel at scico.botik.ru
• [Agda] tracing & profiling   mechvel at scico.botik.ru
• [Agda] equality on Char   mechvel at scico.botik.ru
• [Agda] equality on Char   mechvel at scico.botik.ru
• [Agda] type checking in real-world algebra   mechvel at scico.botik.ru
• [Agda] Why dependent type theory?   mechvel at scico.botik.ru
• [Agda] [Coq-Club] Why dependent type theory?   mechvel at scico.botik.ru
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   mechvel at scico.botik.ru
• [Agda] [Coq-Club] Why dependent type theory?   mechvel at scico.botik.ru
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   mechvel at scico.botik.ru
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   mechvel at scico.botik.ru
• [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 2   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 2   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 2   mechvel at scico.botik.ru
• [Agda] idiom brackets in 2.6.1   mechvel at scico.botik.ru
• [Agda] commutative ring solver   mechvel at scico.botik.ru
• [Agda] An article by Jean-Yves Girard   mechvel at scico.botik.ru
• [Agda] An article by Jean-Yves Girard   mechvel at scico.botik.ru
• [Agda] An article by Jean-Yves Girard   mechvel at scico.botik.ru
• [Agda] An article by Jean-Yves Girard   mechvel at scico.botik.ru
• [Agda] An article by Jean-Yves Girard   mechvel at scico.botik.ru
• [Agda] An article by Jean-Yves Girard   mechvel at scico.botik.ru
• [Agda] An article by Jean-Yves Girard   mechvel at scico.botik.ru
• [Agda] "bug" on x = x   mechvel at scico.botik.ru
• [Agda] An article by Jean-Yves Girard   mechvel at scico.botik.ru
• [Agda] a strange function type report   mechvel at scico.botik.ru
• [Agda] a strange function type report   mechvel at scico.botik.ru
• [Agda] a strange function type report   mechvel at scico.botik.ru
• [Agda] Boolean And in Pair   mechvel at scico.botik.ru
• [Agda] "Failed to find source"   mechvel at scico.botik.ru
• [Agda] many ways to import the same thing from record   mechvel at scico.botik.ru
• [Agda] many ways to import the same thing from record   mechvel at scico.botik.ru
• [Agda] many ways to import the same thing from record   mechvel at scico.botik.ru
• [Agda] many ways to import the same thing from record   mechvel at scico.botik.ru
• [Agda] many ways to import the same thing from record   mechvel at scico.botik.ru
• [Agda] "not in scope" without "does not export"   mechvel at scico.botik.ru
• [Agda] "Cannot resolve" vs "Multiple definition"   mechvel at scico.botik.ru
• [Agda] "open" in record telescope   mechvel at scico.botik.ru
• [Agda] problem with algebraic hierarchy   mechvel at scico.botik.ru
• [Agda] problem with algebraic hierarchy   mechvel at scico.botik.ru
• [Agda] type-checking x=x   mechvel at scico.botik.ru
• [Agda] type-checking x=x   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] Hanging out with the Lean crowd   mechvel at scico.botik.ru
• [Agda] strangely cannot reproduce a report   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda Standard Library 1.4 release candidate 1   mechvel at scico.botik.ru
• [Agda] [ANNOUNCE] Agda Standard Library 1.4 release candidate 1   mechvel at scico.botik.ru
• [Agda] bug?   mechvel at scico.botik.ru
• [Agda] Agda and machine learning   mechvel at scico.botik.ru
• [Agda] Agda and machine learning   mechvel at scico.botik.ru
• [Agda] testing Agda-2.6.1 on a large project   mechvel at scico.botik.ru
• [Agda] Question about inequality and absurd patterns   mechvel at scico.botik.ru
• [Agda] termination problem   mechvel at scico.botik.ru
• [Agda] a strange "unsolved" report   mechvel at scico.botik.ru
• [Agda] a strange "unsolved" report   mechvel at scico.botik.ru
• [Agda] a strange "unsolved" report   mechvel at scico.botik.ru
• [Agda] a strange "unsolved" report   mechvel at scico.botik.ru
• [Agda] a strange "unsolved" report   mechvel at scico.botik.ru
• [Agda] when to set underscore suffix?   mechvel at scico.botik.ru
• [Agda] when to set underscore suffix?   mechvel at scico.botik.ru
• [Agda] when to set underscore suffix?   mechvel at scico.botik.ru
• [Agda] forced arguments in EqReasoning   mechvel at scico.botik.ru
• [Agda] forced arguments in EqReasoning   mechvel at scico.botik.ru
• [Agda] forced arguments in EqReasoning   mechvel at scico.botik.ru
• [Agda] forced arguments in EqReasoning   mechvel at scico.botik.ru
• [Agda] forced arguments in EqReasoning   mechvel at scico.botik.ru
• [Agda] forced arguments in EqReasoning   mechvel at scico.botik.ru
• [Agda] forced arguments in EqReasoning   mechvel at scico.botik.ru
• [Agda] forced arguments in EqReasoning   mechvel at scico.botik.ru
• [Agda] irrelevancy annotation   mechvel at scico.botik.ru
• [Agda] irrelevancy annotation   mechvel at scico.botik.ru
• [Agda] irrelevancy annotation   mechvel at scico.botik.ru
• [Agda] irrelevancy annotation   mechvel at scico.botik.ru
• [Agda] Size Issue when Modelling Effectful Data Structures and Computations   jonas.hoefer at stud.htwk-leipzig.de
• [Agda] Size Issue when Modelling Effectful Data Structures and Computations   jonas.hoefer at stud.htwk-leipzig.de
• [Agda] Size Issue when Modelling Effectful Data Structures and Computations   jonas.hoefer at stud.htwk-leipzig.de
• [Agda] nontermination and Sized types   vlad
• [Agda] nontermination and Sized types   vlad
• [Agda] nontermination and Sized types   vlad
• [Agda] slightly wrong sized datatype definition leads to proof of False   vlad
• [Agda] slightly wrong sized datatype definition leads to proof of False   vlad
• [Agda] slightly wrong sized datatype definition leads to proof of False   vlad
• [Agda] any known proof of ⊥ that does not syntactically use ∞ ?   vlad

Last message date: Thu Dec 31 23:40:10 CET 2020
Archived on: Thu Dec 31 23:40:27 CET 2020

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