2008 Archives by author

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

Starting: Tue Jan 8 02:21:16 CEST 2008
Ending: Tue Dec 30 13:55:38 CEST 2008
Messages: 668

• [Agda] Coinductive datatypes   Álvaro García Pérez
• [Agda] Coinductive datatypes   Álvaro García Pérez
• [Agda] Fwd: Coinductive datatypes   Álvaro García Pérez
• [Agda] Parameterized type families   Álvaro García Pérez
• [Agda] Re: [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad)   Álvaro García Pérez
• [Agda] Emacs Agda mode is not working   Álvaro García Pérez
• [Agda] CADE-22 call for workshop and tutorial proposals   Carsten Schürmann
• [Agda] Agda Installer for Windows   José Pedro Magalhães
• [Agda] Agda Installer for Windows   José Pedro Magalhães
• [Agda] Agda Installer for Windows   José Pedro Magalhães
• [Agda] Unicode in Standard Library   Andrés Sicard-Ramírez
• [Agda] Unicode in Standard Library   Andrés Sicard-Ramírez
• [Agda] a question about name parts   Andrés Sicard-Ramírez
• [Agda] Are the parameters implicit arguments to the constructors?   Andrés Sicard-Ramírez
• [Agda] Unicode in Standard Library   Andreas Abel
• [Agda] LFMTP'08 call for papers   Andreas Abel
• [Agda] Ensuring termination during equality checking   Andreas Abel
• [Agda] Ensuring termination during equality checking   Andreas Abel
• [Agda] LFMTP'08: 2nd Call for Papers   Andreas Abel
• [Agda] Size change of higher order arguments   Andreas Abel
• [Agda] Agda goes coinductive   Andreas Abel
• [Agda] Codata oddity   Andreas Abel
• [Agda] Normalisation before termination checking   Andreas Abel
• [Agda] Status of Prop   Andreas Abel
• [Agda] Parameterized type families   Andreas Abel
• [Agda] trouble with with   Thorsten Altenkirch
• [Agda] trouble with with   Thorsten Altenkirch
• [Agda] coverage in Agda-2.1.3   Thorsten Altenkirch
• [Agda] coverage in Agda-2.1.3   Thorsten Altenkirch
• [Agda] a universe of finite types   Thorsten Altenkirch
• [Agda] problem with C-c | (show context) in 2.1.3   Thorsten Altenkirch
• [Agda] problem with C-c | (show context) in 2.1.3   Thorsten Altenkirch
• [Agda] A plea for Set:Set   Thorsten Altenkirch
• [Agda] A plea for Set:Set   Thorsten Altenkirch
• [Agda] A plea for Set:Set   Thorsten Altenkirch
• [Agda] dependent catch all?   Thorsten Altenkirch
• [Agda] interactive mode   Thorsten Altenkirch
• [Agda] forall in parameters for data   Thorsten Altenkirch
• [Agda] Re: [Coq-Club] Coinductive types and type preservation.   Thorsten Altenkirch
• [Agda] acyclicity of constructors   Thorsten Altenkirch
• [Agda] CFP: Dependently Typed Programming (FI Special Issue)   Thorsten Altenkirch
• [Agda] Lectureship at Nottingham   Thorsten Altenkirch
• [Agda] path?   Thorsten Altenkirch
• [Agda] path?   Thorsten Altenkirch
• [Agda] CFP: PLPV 2009   Thorsten Altenkirch
• [Agda] Big indices for small types?   Thorsten Altenkirch
• [Agda] Final CFP: PLPV 2009   Thorsten Altenkirch
• [Agda] Re: [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad)   Thorsten Altenkirch
• [Agda] Call for participation: PLPV 2009   Thorsten Altenkirch
• [Agda] trouble with "with"   Thorsten Altenkirch
• [Agda] trouble with "with"   Thorsten Altenkirch
• [Agda] How to engage coverage checking   Jim Apple
• Re: [Agda] Why does Data.Product have � for the type constructor?   Lennart Augustsson
• [Agda] Handling the Impossible   Lennart Augustsson
• [Agda] Examples   Lennart Augustsson
• [Agda] Module definition order   Lennart Augustsson
• [Agda] Module definition order   Lennart Augustsson
• [Agda] Lambda   Lennart Augustsson
• [Agda] Lambda   Lennart Augustsson
• [Agda] Re: Lambda   Lennart Augustsson
• [Agda] Re: Lambda   Lennart Augustsson
• [Agda] Re: Lambda   Lennart Augustsson
• Re: [Agda] Why does Data.Product have � for the type constructor?   Marcin Benke
• [Agda] Lambda   Marcin Benke
• [Agda] Type and termination checking around with clauses   Peter Berry
• [Agda] Type and termination checking around with clauses   Peter Berry
• [Agda] Type and termination checking around with clauses   Peter Berry
• Re: [Agda] Why does Data.Product have � for the type constructor?   Peter Berry
• [Agda] Re: [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad)   Aaron Bohannon
• [Agda] Re: [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad)   Aaron Bohannon
• [Agda] Re: [Coq-Club] Re: Agda beats Coq   Aaron Bohannon
• [Agda] [Fwd: Agda post from makoto.takeyama@aist.go.jp requires approval]   Ana Bove
• [Agda] coverage in Agda-2.1.3   Ana Bove
• [Agda] coverage in Agda-2.1.3   Ana Bove
• [Agda] Improving reload performance in emacs mode   Kasper Brink
• [Agda] can normal forms be made to look shorter somehow?   Samuel Bronson
• [Agda] can normal forms be made to look shorter somehow?   Samuel Bronson
• [Agda] Why does Data.Product have � for the type constructor?   Samuel Bronson
• [Agda] Handling the Impossible   Samuel Bronson
• Re: [Agda] Why does Data.Product have � for the type constructor?   Samuel Bronson
• [Agda] Why is refine not working right with "_,_"?   Samuel Bronson
• [Agda] Someone please explain where Set1 comes into this...   Samuel Bronson
• [Agda] Someone please explain where Set1 comes into this...   Samuel Bronson
• [Agda] Why is refine not working right with "_,_"?   Samuel Bronson
• [Agda] A plea for Set:Set   Samuel Bronson
• [Agda] A plea for Set:Set   Samuel Bronson
• [Agda] A plea for Set:Set   Samuel Bronson
• [Agda] C-c C-c not working with module parameters or explicit cases over implicit arguments...   Samuel Bronson
• [Agda] C-c C-c turns issue 64 into a bug   Samuel Bronson
• [Agda] C-c C-c turns issue 64 into a bug   Samuel Bronson
• [Agda] weird error with 'with'   Samuel Bronson
• [Agda] Examples   Samuel Bronson
• [Agda] Library not compiling for me   Samuel Bronson
• [Agda] Module definition order   Samuel Bronson
• [Agda] Agda library patch destination & _darcs/prefs/email   Samuel Bronson
• [Agda] Standard library examples?   Samuel Bronson
• [Agda] Standard library examples?   Samuel Bronson
• [Agda] dependent catch all?   Samuel Bronson
• [Agda] "abstract," Integer, and errors   Samuel Bronson
• [Agda] Lambda   Samuel Bronson
• [Agda] Lambda   Samuel Bronson
• [Agda] Re: Lambda   Samuel Bronson
• [Agda] Difference between two datatypes   Samuel Bronson
• [Agda] interaction/repl when in agda-mode   Jim Burton
• [Agda] interaction/repl when in agda-mode   Jim Burton
• [Agda] Agda-mode: monospaced ucs font for ubuntu?   Jim Burton
• [Agda] Re: Agda-mode: monospaced ucs font for ubuntu?   Jim Burton
• [Agda] non-constructor indices   James Chapman
• [Agda] non-constructor indices   James Chapman
• [Agda] Status of Prop   James Chapman
• [Agda] Status of Prop   James Chapman
• [Agda] Type unification problem in Braun Tree   Liang-Ting Chen
• [Agda] Unicode in Standard Library   IKEGAMI Daisuke
• [Agda] Alpha version of Agda Installer for Windows   IKEGAMI Daisuke
• [Agda] UTF-8 issue in Agda which is built by the latest GHC 6.10.1   IKEGAMI Daisuke
• [Agda] PreorderReasoning not Polymorphic Enough?   Nils Anders Danielsson
• [Agda] PreorderReasoning not Polymorphic Enough?   Nils Anders Danielsson
• [Agda] The archives are now public   Nils Anders Danielsson
• [Agda] Unicode in Standard Library   Nils Anders Danielsson
• [Agda] Just getting into dependent typing   Nils Anders Danielsson
• [Agda] aquamacs gremlins   Nils Anders Danielsson
• [Agda] question about with   Nils Anders Danielsson
• [Agda] .agdai weirdness   Nils Anders Danielsson
• [Agda] heterogeneous equality   Nils Anders Danielsson
• [Agda] The impossible happened.   Nils Anders Danielsson
• [Agda] Re: A patch making Agda smaller and faster   Nils Anders Danielsson
• [Agda] nameless pattern-matching functions   Nils Anders Danielsson
• [Agda] nameless pattern-matching functions   Nils Anders Danielsson
• [Agda] nameless pattern-matching functions   Nils Anders Danielsson
• [Agda] Induction when the argument is wrapped in a constructor?   Nils Anders Danielsson
• [Agda] Announcement: Agda FFI   Nils Anders Danielsson
• [Agda] IO design dangers   Nils Anders Danielsson
• [Agda] Induction when the argument is wrapped in a constructor?   Nils Anders Danielsson
• [Agda] Induction when the argument is wrapped in a constructor?   Nils Anders Danielsson
• [Agda] Injectivity of Constructors?   Nils Anders Danielsson
• [Agda] Size change of higher order arguments   Nils Anders Danielsson
• [Agda] wishlist/some help wanted   Nils Anders Danielsson
• [Agda] wishlist/some help wanted   Nils Anders Danielsson
• [Agda] Type and termination checking around with clauses   Nils Anders Danielsson
• [Agda] Type and termination checking around with clauses   Nils Anders Danielsson
• [Agda] Type and termination checking around with clauses   Nils Anders Danielsson
• [Agda] trouble with with   Nils Anders Danielsson
• [Agda] Help with proofs   Nils Anders Danielsson
• [Agda] Equality of arguments in Agda   Nils Anders Danielsson
• [Agda] Help with proofs   Nils Anders Danielsson
• [Agda] A plea for Set:Set   Nils Anders Danielsson
• [Agda] A plea for Set:Set   Nils Anders Danielsson
• [Agda] A plea for Set:Set   Nils Anders Danielsson
• [Agda] A plea for Set:Set   Nils Anders Danielsson
• [Agda] With and the inspect idiom   Nils Anders Danielsson
• [Agda] weird error with 'with'   Nils Anders Danielsson
• [Agda] emacs hangs when loading agda2-mode   Nils Anders Danielsson
• [Agda] Examples   Nils Anders Danielsson
• [Agda] Examples   Nils Anders Danielsson
• [Agda] Library not compiling for me   Nils Anders Danielsson
• [Agda] Module definition order   Nils Anders Danielsson
• [Agda] Module definition order   Nils Anders Danielsson
• [Agda] Re: Agda library patch destination & _darcs/prefs/email   Nils Anders Danielsson
• [Agda] Module definition order   Nils Anders Danielsson
• [Agda] emacs agda mode on apple mac os x   Nils Anders Danielsson
• [Agda] dependent catch all?   Nils Anders Danielsson
• [Agda] Codata oddity   Nils Anders Danielsson
• [Agda] Re: Codata oddity   Nils Anders Danielsson
• [Agda] Agda goes coinductive   Nils Anders Danielsson
• [Agda] Codata oddity   Nils Anders Danielsson
• [Agda] Terminology: inductive family   Nils Anders Danielsson
• [Agda] interactive mode   Nils Anders Danielsson
• [Agda] interactive mode   Nils Anders Danielsson
• [Agda] forall in parameters for data   Nils Anders Danielsson
• [Agda] forall in parameters for data   Nils Anders Danielsson
• [Agda] Reference manual   Nils Anders Danielsson
• [Agda] "abstract," Integer, and errors   Nils Anders Danielsson
• [Agda] Lambda   Nils Anders Danielsson
• [Agda] Lambda   Nils Anders Danielsson
• [Agda] Agda and Aquamacs   Nils Anders Danielsson
• [Agda] Lambda   Nils Anders Danielsson
• [Agda] Agda and Aquamacs   Nils Anders Danielsson
• [Agda] Lambda   Nils Anders Danielsson
• [Agda] Lambda   Nils Anders Danielsson
• [Agda] Agda and Aquamacs   Nils Anders Danielsson
• [Agda] Difference between two datatypes   Nils Anders Danielsson
• [Agda] Lambda   Nils Anders Danielsson
• [Agda] Difference between two datatypes   Nils Anders Danielsson
• [Agda] acyclicity of constructors   Nils Anders Danielsson
• [Agda] "Not in scope" error   Nils Anders Danielsson
• [Agda] "Not in scope" error   Nils Anders Danielsson
• [Agda] "Not in scope" error   Nils Anders Danielsson
• [Agda] "Not in scope" error   Nils Anders Danielsson
• [Agda] "Not in scope" error   Nils Anders Danielsson
• [Agda] include directories and agda-mode "warping" between files   Nils Anders Danielsson
• [Agda] Agda Installer for Windows   Nils Anders Danielsson
• [Agda] broken   Nils Anders Danielsson
• [Agda] New Agda-specific input method   Nils Anders Danielsson
• [Agda] Normalisation before termination checking   Nils Anders Danielsson
• [Agda] Normalisation before termination checking   Nils Anders Danielsson
• [Agda] Normalisation before termination checking   Nils Anders Danielsson
• [Agda] Normalisation before termination checking   Nils Anders Danielsson
• [Agda] PrettyPrint.agda   Nils Anders Danielsson
• [Agda] Debian packages   Nils Anders Danielsson
• [Agda] PrettyPrint.agda   Nils Anders Danielsson
• [Agda] Codata and "with" matching   Nils Anders Danielsson
• [Agda] Codata and "with" matching   Nils Anders Danielsson
• [Agda] Status of Prop   Nils Anders Danielsson
• [Agda] Re: A patch to agda2-mode.el   Nils Anders Danielsson
• [Agda] Status of Prop   Nils Anders Danielsson
• [Agda] Questions regarding non-constructor indexed datatypes   Nils Anders Danielsson
• [Agda] Indexed Monads   Nils Anders Danielsson
• [Agda] Parameterized type families   Nils Anders Danielsson
• [Agda] Parameterized type families   Nils Anders Danielsson
• [Agda] lhs2TeX-1.14 with Agda support   Nils Anders Danielsson
• [Agda] interaction/repl when in agda-mode   Nils Anders Danielsson
• [Agda] Type unification problem in Braun Tree   Nils Anders Danielsson
• [Agda] UTF-8 issue in Agda which is built by the latest GHC 6.10.1   Nils Anders Danielsson
• [Agda] Avoid GHC 6.10.1 (for now)   Nils Anders Danielsson
• [Agda] Data.Nat error   Nils Anders Danielsson
• [Agda] Data.Nat error   Nils Anders Danielsson
• [Agda] Data.Nat error   Nils Anders Danielsson
• [Agda] Compiling Everything.agda   Nils Anders Danielsson
• [Agda] Compiling Everything.agda   Nils Anders Danielsson
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Nils Anders Danielsson
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Nils Anders Danielsson
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Nils Anders Danielsson
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Nils Anders Danielsson
• [Agda] (long post) some semantics, some syntax   Nils Anders Danielsson
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Nils Anders Danielsson
• [Agda] Any Mac volunteers?   Nils Anders Danielsson
• [Agda] Re: Lambda   Nils Anders Danielsson
• [Agda] problem in installing QuickCheck   Nils Anders Danielsson
• [Agda] () is not a valid expression   Nils Anders Danielsson
• [Agda] Termination proof in partiality monad   Nils Anders Danielsson
• [Agda] () is not a valid expression   Nils Anders Danielsson
• [Agda] () is not a valid expression   Nils Anders Danielsson
• [Agda] Termination proof in partiality monad   Nils Anders Danielsson
• [Agda] () is not a valid expression   Nils Anders Danielsson
• [Agda] During and after the Agda installation   Nils Anders Danielsson
• [Agda] Re: Agda beats Coq   Nils Anders Danielsson
• [Agda] Mixing = and ~   Nils Anders Danielsson
• [Agda] Re: Agda beats Coq   Nils Anders Danielsson
• [Agda] Some newbie questions   Nils Anders Danielsson
• [Agda] Agda-mode: monospaced ucs font for ubuntu?   Nils Anders Danielsson
• [Agda] Agda-mode: monospaced ucs font for ubuntu?   Nils Anders Danielsson
• [Agda] Using Data.Sets   Nils Anders Danielsson
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Nils Anders Danielsson
• [Agda] Emacs Agda mode is not working   Nils Anders Danielsson
• [Agda] Positivity checker   Nils Anders Danielsson
• [Agda] Positivity checker   Nils Anders Danielsson
• [Agda] Re: Mixing = and ~   Nils Anders Danielsson
• [Agda] AIM 9 summary   Nils Anders Danielsson
• [Agda] Re: Agda beats Coq   Nils Anders Danielsson
• [Agda] Positivity checker   Nils Anders Danielsson
• [Agda] Positivity checker   Nils Anders Danielsson
• [Agda] agda --html   Nils Anders Danielsson
• [Agda] Re: Lambda   Nils Anders Danielsson
• [Agda] trouble with "with"   Nils Anders Danielsson
• [Agda] trouble with "with"   Nils Anders Danielsson
• [Agda] Indexed Monads   Dan Doel
• [Agda] Indexed Monads   Dan Doel
• [Agda] The impossible happened.   Dan Doel
• [Agda] Inductive indexing   Dan Doel
• [Agda] Inductive indexing   Dan Doel
• [Agda] Agda goes coinductive   Dan Doel
• [Agda] Agda goes coinductive   Dan Doel
• [Agda] Agda goes coinductive   Dan Doel
• [Agda] Agda goes coinductive   Dan Doel
• [Agda] Agda goes coinductive   Dan Doel
• [Agda] Getting codata right   Dan Doel
• [Agda] Parameterized type families   Dan Doel
• [Agda] Termination proof in partiality monad   Dan Doel
• [Agda] Termination proof in partiality monad   Dan Doel
• [Coq-Club] Re: [Agda] Termination proof in partiality monad   Dan Doel
• [Agda] Termination proof in partiality monad   Dan Doel
• [Agda] Termination proof in partiality monad   Dan Doel
• [Agda] Re: Agda beats Coq (was: Termination proof in partiality monad)   Dan Doel
• [Agda] Re: [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad)   Dan Doel
• [Agda] Re: [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad)   Dan Doel
• [Agda] Re: [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad)   Dan Doel
• [Agda] Re: [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad)   Dan Doel
• [Agda] Re: [Coq-Club] Re: Agda beats Coq   Dan Doel
• [Agda] "Not in scope" error   Antoine Durand-Gasselin
• [Agda] Dependent Types at Work   Peter Dybjer
• [Agda] Dependent Types at Work   Peter Dybjer
• [Agda] Dependent Types at Work   Peter Dybjer
• [Agda] Size change of higher order arguments   Peter Dybjer
• [Agda] Terminology: inductive family   Peter Dybjer
• [Agda] Terminology: inductive family   Peter Dybjer
• [Agda] Terminology: inductive family   Peter Dybjer
• [Agda] Terminology: inductive family   Peter Dybjer
• [Agda] Big indices for small types?   Peter Dybjer
• [Agda] Warning: this message contains amateur philosophy   Peter Dybjer
• [Agda] Positivity checker   Peter Dybjer
• [Agda] Positivity checker   Peter Dybjer
• [Agda] Positivity checker   Peter Dybjer
• [Agda] Positivity checker   Peter Dybjer
• [Agda] Positivity checker   Peter Dybjer
• [Agda] Possible bug   Chris Eidhof
• [Agda] interactive mode   Chris Eidhof
• [Agda] Twelf Tutorial (Call for participation)   Twelf Elf
• [Agda] emacs agda mode on apple mac os x   WILSON F.A.J.
• [Agda] agda2-mode highlighting   WILSON F.A.J.
• [Agda] Agda and Aquamacs   WILSON F.A.J.
• [Agda] include directories and agda-mode "warping" between files   WILSON F.A.J.
• [Agda] include directories and agda-mode "warping" between files   WILSON F.A.J.
• [Agda] Debian packages   Liyang HU
• [Agda] Re: Debian packages   Liyang HU
• [Agda] non-constructor indices   Peter Hancock
• [Agda] Terminology: inductive family   Peter Hancock
• [Agda] Terminology: inductive family   Peter Hancock
• [Agda] Terminology: inductive family   Peter Hancock
• [Agda] Terminology: inductive family   Peter Hancock
• [Agda] Terminology: inductive family   Peter Hancock
• [Agda] Positivity checker   Peter Hancock
• [Agda] Positivity checker   Peter Hancock
• [Agda] Leibniz & Co   Sebastian Hanowski
• [Agda] Leibniz & Co (and no Unicode)   Sebastian Hanowski
• [Agda] Hindas 2002 flashback   Sebastian Hanowski
• [Agda] Borring question: Cabal, compiling for linux-ppc   Pierre Hyvernat
• [Agda] Research Position on HermiT project at Oxford University Computing Laboratory   Ian.Horrocks at comlab.ox.ac.uk
• [Agda] D.Phil (PhD) Studentship on ConDOR project at Oxford University Computing Laboratory   Ian.Horrocks at comlab.ox.ac.uk
• [Agda] Installing from darcs   J.Burton at brighton.ac.uk
• [Agda] Installing from darcs   J.Burton at brighton.ac.uk
• [Agda] heterogeneous lists with universes   J.Burton at brighton.ac.uk
• [Agda] heterogeneous lists with universes   J.Burton at brighton.ac.uk
• [Agda] heterogeneous lists with universes   J.Burton at brighton.ac.uk
• [Agda] () is not a valid expression   J.Burton at brighton.ac.uk
• [Agda] () is not a valid expression   J.Burton at brighton.ac.uk
• [Agda] () is not a valid expression   J.Burton at brighton.ac.uk
• [Agda] () is not a valid expression   J.Burton at brighton.ac.uk
• [Agda] Some newbie questions   J.Burton at brighton.ac.uk
• [Agda] Some newbie questions   J.Burton at brighton.ac.uk
• [Agda] Using Data.Sets   J.Burton at brighton.ac.uk
• [Agda] Using Data.Sets   J.Burton at brighton.ac.uk
• [Agda] Agda-mode: monospaced ucs font for ubuntu?   J.Burton at brighton.ac.uk
• [Agda] non-constructor indices   Patrik Jansson
• [Agda] Agda goes coinductive   Edward Kmett
• [Agda] Lambda   Edward Kmett
• [Coq-Club] Re: [Agda] Termination proof in partiality monad   Vladimir Komendantsky
• [Coq-Club] Re: [Agda] Termination proof in partiality monad   Vladimir Komendantsky
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Iain Lane
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Iain Lane
• [Agda] "abstract," Integer, and errors   Sean Leather
• [Agda] Agda and Aquamacs   Sean Leather
• [Agda] Agda and Aquamacs   Sean Leather
• [Agda] Agda and Aquamacs   Sean Leather
• [Agda] Difference between two datatypes   Sean Leather
• [Agda] Agda and Aquamacs   Sean Leather
• [Agda] Difference between two datatypes   Sean Leather
• [Agda] Implicit argument with type function   Sean Leather
• [Agda] Implicit argument with type function   Sean Leather
• [Agda] problem in installing alex and darcs using macports   Gyesik Lee
• [Agda] problem in installing alex and darcs using macports   Gyesik Lee
• [Agda] problem in installing QuickCheck   Gyesik Lee
• [Agda] problem in installing QuickCheck   Gyesik Lee
• [Agda] During and after the Agda installation   Gyesik Lee
• [Agda] Positivity checker   Gyesik Lee
• [Agda] Positivity checker   Gyesik Lee
• [Agda] Re: [Coq-Club] Re: Agda beats Coq   Xavier Leroy
• [Agda] non-constructor indices   Dan Licata
• [Agda] emptiness checking with strings   Dan Licata
• [Agda] emptiness checking with strings   Dan Licata
• [Agda] Re: [Haskell-cafe] Signature for non-empty filter   Dan Licata
• [Agda] Just getting into dependent typing   Dan Licata
• [Agda] question about with   Dan Licata
• [Agda] aquamacs gremlins   Dan Licata
• [Agda] heterogeneous equality   Dan Licata
• [Agda] heterogeneous equality   Dan Licata
• [Agda] nameless pattern-matching functions   Dan Licata
• [Agda] Dependent Types at Work   Dan Licata
• [Agda] Dependent Types at Work   Dan Licata
• [Agda] Dependent Types at Work   Dan Licata
• [Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)   Dan Licata
• [Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)   Dan Licata
• [Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)   Dan Licata
• [Agda] Getting codata right   Dan Licata
• [Agda] acyclicity of constructors   Dan Licata
• [Agda] acyclicity of constructors   Dan Licata
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Dan Licata
• [Agda] (long post) some semantics, some syntax   Dan Licata
• [Agda] Positivity checker   Dan Licata
• [Agda] Twelf Tutorial: Second Call for Participation   Dan Licata
• [Agda] Possible bug   Andres Loeh
• [Agda] interactive mode   Andres Loeh
• [Agda] interactive mode   Andres Loeh
• [Agda] interactive mode   Andres Loeh
• [Agda] interactive mode   Andres Loeh
• [Agda] Status of Prop   Andres Loeh
• [Agda] Status of Prop   Andres Loeh
• [Agda] lhs2TeX-1.14 with Agda support   Andres Loeh
• [Agda] lhs2TeX-1.14 with Agda support   Andres Loeh
• [Agda] heterogeneous lists with universes   Andres Loeh
• [Agda] Just getting into dependent typing   Conor McBride
• [Agda] aquamacs gremlins   Conor McBride
• [Agda] .agdai weirdness   Conor McBride
• [Agda] .agdai weirdness   Conor McBride
• [Agda] heterogeneous equality   Conor McBride
• [Agda] heterogeneous equality   Conor McBride
• [Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)   Conor McBride
• [Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)   Conor McBride
• [Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)   Conor McBride
• [Agda] vector foldl Miller magic?   Conor McBride
• [Agda] Size change of higher order arguments   Conor McBride
• [Agda] coverage in Agda-2.1.3   Conor McBride
• [Agda] With and the inspect idiom   Conor McBride
• [Agda] Termination   Conor McBride
• [Agda] Agda goes coinductive   Conor McBride
• [Agda] Codata oddity   Conor McBride
• [Agda] Agda goes coinductive   Conor McBride
• [Agda] Codata oddity   Conor McBride
• [Agda] Getting codata right   Conor McBride
• [Agda] no quick cofix   Conor McBride
• [Agda] Terminology: inductive family   Conor McBride
• [Agda] interactive mode   Conor McBride
• [Agda] acyclicity of constructors   Conor McBride
• [Agda] acyclicity of constructors   Conor McBride
• [Agda] some yellow, for your amusement   Conor McBride
• [Agda] some yellow, for your amusement   Conor McBride
• [Agda] primitive recursion over the natural numbers   Conor McBride
• [Agda] Big indices for small types?   Conor McBride
• [Agda] Status of Prop   Conor McBride
• [Agda] Status of Prop   Conor McBride
• [Agda] Hindas 2002 flashback   Conor McBride
• [Agda] Strange normalization   Conor McBride
• [Agda] Parameterized type families   Conor McBride
• [Agda] (long post) some semantics, some syntax   Conor McBride
• [Agda] Re: Lambda   Stefan Monnier
• [Agda] Re: Agda-mode: monospaced ucs font for ubuntu?   Stefan Monnier
• [Agda] Re: Emacs Agda mode is not working   Stefan Monnier
• [Agda] primitive recursion over the natural numbers   Ed Morehouse
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Darin Morrison
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Darin Morrison
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Darin Morrison
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Darin Morrison
• [Agda] Some newbie questions   Darin Morrison
• [Agda] Using Data.Sets   Darin Morrison
• [Agda] Unicode in Standard Library   Shin-Cheng Mu
• [Agda] Duplicate binding for built-in thing   Shin-Cheng Mu
• [Agda] Duplicate binding for built-in thing   Shin-Cheng Mu
• [Agda] Induction when the argument is wrapped in a constructor?   Shin-Cheng Mu
• [Agda] Induction when the argument is wrapped in a constructor?   Shin-Cheng Mu
• [Agda] Induction when the argument is wrapped in a constructor?   Shin-Cheng Mu
• [Agda] Magic-with and inspect -- can I have both?   Shin-Cheng Mu
• [Agda] Injectivity of Constructors?   Shin-Cheng Mu
• [Agda] Size change of higher order arguments   Shin-Cheng Mu
• [Agda] With and the inspect idiom   Shin-Cheng Mu
• [Agda] With and the inspect idiom   Shin-Cheng Mu
• [Agda] With and the inspect idiom   Shin-Cheng Mu
• [Agda] With and the inspect idiom   Shin-Cheng Mu
• [Agda] Abusing the GADT syntax   Shin-Cheng Mu
• [Agda] Codata and "with" matching   Shin-Cheng Mu
• [Agda] Codata and "with" matching   Shin-Cheng Mu
• [Agda] Questions regarding non-constructor indexed datatypes   Shin-Cheng Mu
• [Agda] Termination proof in partiality monad   Shin-Cheng Mu
• [Agda] hs-cabal binary for OS X   Shin-Cheng Mu
• Re: [Agda] Why does Data.Product have � for the type constructor?   Bengt Nordstrom
• [Agda] Lambda   Bengt Nordstrom
• [Agda] non-constructor indices   Ulf Norell
• [Agda] emptiness checking with strings   Ulf Norell
• [Agda] Indexed Monads   Ulf Norell
• [Agda] Just getting into dependent typing   Ulf Norell
• Fwd: [Agda] question about with   Ulf Norell
• [Agda] .agdai weirdness   Ulf Norell
• [Agda] .agdai weirdness   Ulf Norell
• [Agda] Ensuring termination during equality checking   Ulf Norell
• [Agda] heterogeneous equality   Ulf Norell
• [Agda] Duplicate binding for built-in thing   Ulf Norell
• [Agda] termination & open public   Ulf Norell
• [Agda] termination & open public   Ulf Norell
• [Agda] The wiki is back up   Ulf Norell
• [Agda] a question about name parts   Ulf Norell
• [Agda] Induction when the argument is wrapped in a constructor?   Ulf Norell
• [Agda] Announcement: Agda FFI   Ulf Norell
• [Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)   Ulf Norell
• [Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)   Ulf Norell
• [Agda] Alternative partial function attempt   Ulf Norell
• [Agda] Unexpected successful loading of silly program   Ulf Norell
• [Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)   Ulf Norell
• [Agda] Problem with inductively defined type having (simulated) partial constructors   Ulf Norell
• [Agda] Help with proofs   Ulf Norell
• [Agda] Type and termination checking around with clauses   Ulf Norell
• [Agda] Type and termination checking around with clauses   Ulf Norell
• [Agda] Type and termination checking around with clauses   Ulf Norell
• [Agda] Type and termination checking around with clauses   Ulf Norell
• [Agda] Equality of arguments in Agda   Ulf Norell
• [Agda] coverage in Agda-2.1.3   Ulf Norell
• [Agda] can normal forms be made to look shorter somehow?   Ulf Norell
• [Agda] Possible bug   Ulf Norell
• [Agda] problem with C-c | (show context) in 2.1.3   Ulf Norell
• [Agda] Handling the Impossible   Ulf Norell
• [Agda] Handling the Impossible   Ulf Norell
• [Agda] Why is refine not working right with "_,_"?   Ulf Norell
• [Agda] Someone please explain where Set1 comes into this...   Ulf Norell
• [Agda] With and the inspect idiom   Ulf Norell
• [Agda] Why is refine not working right with "_,_"?   Ulf Norell
• [Agda] A plea for Set:Set   Ulf Norell
• [Agda] With and the inspect idiom   Ulf Norell
• [Agda] C-c C-c not working with module parameters or explicit cases over implicit arguments...   Ulf Norell
• [Agda] C-c C-c turns issue 64 into a bug   Ulf Norell
• [Agda] C-c C-c turns issue 64 into a bug   Ulf Norell
• [Agda] A plea for Set:Set   Ulf Norell
• [Agda] Problems trying to build Agda   Ulf Norell
• [Agda] emacs hangs when loading agda2-mode   Ulf Norell
• [Agda] Abusing the GADT syntax   Ulf Norell
• [Agda] Borring question: Cabal, compiling for linux-ppc   Ulf Norell
• [Agda] Module definition order   Ulf Norell
• [Agda] Module definition order   Ulf Norell
• [Agda] Agda-2.1.3 build error   Ulf Norell
• [Agda] Agda goes coinductive   Ulf Norell
• [Agda] Agda goes coinductive   Ulf Norell
• [Agda] executable?   Ulf Norell
• [Agda] interactive mode   Ulf Norell
• [Agda] forall in parameters for data   Ulf Norell
• [Agda] agda2-mode highlighting   Ulf Norell
• [Agda] Are the parameters implicit arguments to the constructors?   Ulf Norell
• [Agda] Re: Lambda   Ulf Norell
• [Agda] Some documentation on agda   Ulf Norell
• [Agda] path?   Ulf Norell
• [Agda] some yellow, for your amusement   Ulf Norell
• [Agda] some yellow, for your amusement   Ulf Norell
• [Agda] Agda moves to haskell.org   Ulf Norell
• [Agda] Status of Prop   Ulf Norell
• [Agda] basic question about induction/recursion & pattern-matching   Ulf Norell
• [Agda] Coinductive datatypes   Ulf Norell
• [Agda] Fwd: Coinductive datatypes   Ulf Norell
• [Agda] Strange normalization   Ulf Norell
• [Agda] Questions regarding non-constructor indexed datatypes   Ulf Norell
• [Agda] Absurd lambdas   Ulf Norell
• [Agda] Absurd lambdas   Ulf Norell
• [Agda] implicit argument equality weirdness   Ulf Norell
• [Agda] interaction/repl when in agda-mode   Ulf Norell
• [Agda] interaction/repl when in agda-mode   Ulf Norell
• [Agda] Installing from darcs   Ulf Norell
• [Agda] Installing from darcs   Ulf Norell
• [Agda] Installing from darcs   Ulf Norell
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Ulf Norell
• [Agda] problem in installing alex and darcs using macports   Ulf Norell
• [Agda] How to engage coverage checking   Ulf Norell
• [Agda] Improving reload performance in emacs mode   Ulf Norell
• [Agda] Positivity checker   Ulf Norell
• [Agda] Just getting into dependent typing   Luke Palmer
• [Agda] Termination proof in partiality monad   Luke Palmer
• [Coq-Club] Re: [Agda] Termination proof in partiality monad   Luke Palmer
• [Agda] TLCA'09 - Preliminary Call for Papers   Luca Paolini
• [Agda] TLCA 09 - Call for Paper - Update   Luca Paolini
• [Agda] TLCA' 09: Final Call for Papers   Luca Paolini
• [Agda] TLCA'09 Last Call For Paper   Luca Paolini
• [Agda] Finall Call For Papers (DSL WC)   Emir Pasalic
• [Agda] Equality of arguments in Agda   Robert Rothenberg
• [Agda] Type inference question   Robert Rothenberg
• [Agda] Type inference question   Robert Rothenberg
• [Agda] "Not in scope" error   Robert Rothenberg
• [Agda] "Not in scope" error   Robert Rothenberg
• [Agda] "Not in scope" error   Robert Rothenberg
• [Agda] "Not in scope" error   Robert Rothenberg
• [Agda] Re: ANNOUNCE: Haskell Communities and Activities Report (15th ed., November 2008)   Benjamin L. Russell
• [Agda] CADE-22 first call for papers   Carsten Schuermann
• [Agda] Type and termination checking around with clauses   Anton Setzer
• [Agda] Type and termination checking around with clauses   Anton Setzer
• [Agda] With and the inspect idiom   Anton Setzer
• [Agda] Codata oddity   Anton Setzer
• [Agda] Codata oddity   Anton Setzer
• [Agda] Getting codata right   Anton Setzer
• [Agda] Getting codata right   Anton Setzer
• [Agda] Lambda   Anton Setzer
• [Agda] Some documentation on agda   Anton Setzer
• [Agda] Lambda   Anton Setzer
• [Agda] Agda goes coinductive   Anton Setzer
• [Agda] Normalisation before termination checking   Anton Setzer
• [Agda] Termination proof in partiality monad   Anton Setzer
• [Agda] Parameterized type families   Matthieu Sozeau
• [Agda] Re: Agda beats Coq   Matthieu Sozeau
• [Agda] Normalisation before termination checking   Arnaud Spiwack
• [Agda] Re: [Coq-Club] Re: Agda beats Coq   Arnaud Spiwack
• [Agda] Re: [Coq-Club] Re: Agda beats Coq   Arnaud Spiwack
• [Agda] Re: [Coq-Club] Re: Agda beats Coq   Arnaud Spiwack
• [Agda] Strange normalization   Sam Staton
• [Agda] Re: [Haskell-cafe] ANNOUNCE: Haskell Communities and Activities Report (15th ed., November 2008)   Don Stewart
• [Agda] Inductive indexing   Wouter Swierstra
• [Agda] Problem with inductively defined type having (simulated) partial constructors   Wouter Swierstra
• [Agda] Problem with inductively defined type having (simulated) partial constructors   Wouter Swierstra
• [Agda] Problem with inductively defined type having (simulated) partial constructors   Wouter Swierstra
• [Agda] Help with proofs   Wouter Swierstra
• [Agda] A plea for Set:Set   Wouter Swierstra
• [Agda] executable?   Wouter Swierstra
• [Agda] Agda and Aquamacs   Wouter Swierstra
• [Agda] Difference between two datatypes   Wouter Swierstra
• [Agda] Difference between two datatypes   Wouter Swierstra
• [Agda] Implicit argument with type function   Wouter Swierstra
• [Agda] Implicit argument with type function   Wouter Swierstra
• [Agda] Status of Prop   Wouter Swierstra
• [Agda] basic question about induction/recursion & pattern-matching   Wouter Swierstra
• [Agda] () is not a valid expression   Wouter Swierstra
• [Agda] Positivity checker   Wouter Swierstra
• [Agda] Positivity checker   Wouter Swierstra
• [Agda] Positivity checker   Wouter Swierstra
• [Agda] Alpha version of Agda Installer for Windows   Makoto Takeyama
• [Agda] Alpha version of Agda Installer for Windows   Makoto Takeyama
• [Agda] Windows Agda2 Installer, 3rd try   Makoto Takeyama
• [Agda] .agdai weirdness   Makoto Takeyama
• [Agda] Re: A patch making Agda smaller and faster   Makoto Takeyama
• [Agda] a new compiler MAlonzo   Makoto Takeyama
• [Agda] new option -no-injectivity-check   Makoto Takeyama
• [Agda] Re: a new compiler MAlonzo   Makoto Takeyama
• [Agda] Agda Installer for Windows   Makoto Takeyama
• [Agda] Agda Installer for Windows   Makoto Takeyama
• [Agda] A patch for Windows   Makoto Takeyama
• [Agda] Re: A patch to agda2-mode.el   Makoto Takeyama
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Makoto Takeyama
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Makoto Takeyama
• [Agda] Re: Avoid GHC 6.10.1 (for now)   Makoto Takeyama
• [Agda] Re: [Haskell-cafe] Signature for non-empty filter   Henning Thielemann
• [Agda] A plea for Set:Set   Remi Turk
• [Agda] interactive mode   Remi Turk
• [Agda] Second Call for Papers: Special issue of AMAI on CFVAI   Miroslav Velev
• [Agda] problem in installing QuickCheck   Andrea Vezzosi
• [Agda] ANNOUNCE: Haskell Communities and Activities Report (15th ed., November 2008)   Janis Voigtlaender
• [Agda] Termination proof in partiality monad   Edsko de Vries
• [Agda] Termination proof in partiality monad   Edsko de Vries
• [Coq-Club] Re: [Agda] Termination proof in partiality monad   Edsko de Vries
• [Agda] Agda beats Coq (was: Termination proof in partiality monad)   Edsko de Vries
• [Coq-Club] Re: [Agda] Termination proof in partiality monad   Edsko de Vries
• [Agda] Problems trying to build Agda   Geoffrey Alan Washburn
• [Agda] Re: Problems trying to build Agda   Geoffrey Alan Washburn
• [Agda] Standard library examples?   Geoffrey Alan Washburn
• [Agda] Termination   Geoffrey Alan Washburn
• [Agda] Dependent Types at Work   Tristan Wibberley
• [Agda] Dependent Types at Work   Tristan Wibberley
• [Agda] Dependent Types at Work   Tristan Wibberley
• [Agda] Dependent Types at Work   Tristan Wibberley
• [Agda] Dependent Types at Work   Tristan Wibberley
• [Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)   Tristan Wibberley
• [Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)   Tristan Wibberley
• [Agda] IO design dangers   Tristan Wibberley
• [Agda] Unexpected successful loading of silly program   Tristan Wibberley
• [Agda] Alternative partial function attempt   Tristan Wibberley
• [Agda] IO design dangers   Tristan Wibberley
• [Agda] Problem with inductively defined type having (simulated) partial constructors   Tristan Wibberley
• [Agda] Problem with inductively defined type having (simulated) partial constructors   Tristan Wibberley
• [Agda] Problem with inductively defined type having (simulated) partial constructors   Tristan Wibberley
• [Agda] Problem with inductively defined type having (simulated) partial constructors   Tristan Wibberley
• [Agda] wishlist/some help wanted   Tristan Wibberley
• [Agda] Help with proofs   Tristan Wibberley
• [Agda] wishlist/some help wanted   Tristan Wibberley
• [Agda] Help with proofs   Tristan Wibberley
• [Agda] Help with proofs   Tristan Wibberley
• [Agda] PrettyPrint.agda   Yoriyuki Yamagata
• [Agda] PrettyPrint.agda   Yoriyuki Yamagata
• [Agda] PrettyPrint.agda   Yoriyuki Yamagata
• [Agda] emacs hangs when loading agda2-mode   Brent Yorgey
• [Agda] emacs hangs when loading agda2-mode   Brent Yorgey
• [Agda] AIM9   KINOSHITA Yoshiki
• [Agda] AIM9 program update   KINOSHITA Yoshiki
• [Agda] nameless pattern-matching functions   Noam Zeilberger
• [Agda] nameless pattern-matching functions   Noam Zeilberger
• [Agda] termination & open public   Noam Zeilberger
• [Agda] Type inference question   Noam Zeilberger
• [Agda] basic question about induction/recursion & pattern-matching   Noam Zeilberger
• [Agda] Absurd lambdas   Noam Zeilberger
• [Agda] implicit argument equality weirdness   Noam Zeilberger
• [Agda] implicit argument equality weirdness   Noam Zeilberger
• [Agda] Agda-2.1.3 build error   Ruben Henner Zilibowitz
• [Agda] executable?   Ruben Henner Zilibowitz
• [Agda] broken   Ruben Henner Zilibowitz
• [Agda] broken   Ruben Henner Zilibowitz
• [Agda] Data.Nat error   Ruben Henner Zilibowitz
• [Agda] Data.Nat error   Ruben Henner Zilibowitz
• [Agda] Data.Nat error   Ruben Henner Zilibowitz
• [Agda] Compiling Everything.agda   Ruben Henner Zilibowitz
• [Agda] Ornamental Algebras, Algebraic Ornaments   conor at strictlypositive.org
• [Agda] MULTICONF-09 call for papers   Peter james

Last message date: Tue Dec 30 13:55:38 CEST 2008
Archived on: Tue Dec 30 14:00:07 CEST 2008

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