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