RecentChanges

Totality . . . July 03, 2020, at 08:35 AM by Fabian Kunze fabiankunzecsuni-saarlandde: Coq allows allows more than just primitive recursive definitions, for example fib.
Prop . . . December 14, 2018, at 06:39 PM by ?:
Overview . . . December 14, 2018, at 06:38 PM by ?:
Non-recursiveResolutionForInstanceArguments . . . December 14, 2018, at 06:37 PM by ?:
ModellingTypeClassesWithInstanceArguments . . . December 14, 2018, at 06:36 PM by ?:
CoreSyntax . . . December 14, 2018, at 06:35 PM by ?:
BadInHaskell . . . December 14, 2018, at 06:35 PM by ?:
Compiler . . . December 14, 2018, at 06:33 PM by ?:
Emacs . . . December 14, 2018, at 06:31 PM by ?:
Mutual . . . December 14, 2018, at 06:31 PM by ?:
PatternMatchingLambdas . . . December 14, 2018, at 06:30 PM by ?:
Codatatypes . . . December 14, 2018, at 06:30 PM by ?:
LexicalMatters . . . December 14, 2018, at 06:29 PM by ?:
ImplicitArg . . . December 14, 2018, at 06:29 PM by ?:
LocalDefinition . . . December 14, 2018, at 06:28 PM by ?:
With-expression . . . December 14, 2018, at 06:27 PM by ?:
ParameterizedInductiveTypes . . . December 14, 2018, at 06:26 PM by ?:
SimpleInductiveTypes . . . December 14, 2018, at 06:26 PM by ?:
InductiveDataTypesAndPatternMatching . . . December 14, 2018, at 06:25 PM by ?:
FindingTheValuesOfImplicitArguments . . . December 14, 2018, at 06:24 PM by ?:
StructureOfAnAgdaProgram . . . December 14, 2018, at 06:22 PM by ?:
IntroWhat . . . December 14, 2018, at 05:39 PM by ?:
StandardLibrary . . . December 14, 2018, at 05:24 PM by ?:
LiterateAgda . . . December 14, 2018, at 05:19 PM by ?:
ForeignFunctionInterface . . . December 14, 2018, at 05:18 PM by ?:
Compilation . . . December 14, 2018, at 05:18 PM by ?:
Pragmas . . . December 14, 2018, at 05:17 PM by ?:
Irrelevance . . . December 14, 2018, at 05:15 PM by ?:
Reflection . . . December 14, 2018, at 05:13 PM by ?:
UniversePolymorphism . . . December 14, 2018, at 05:12 PM by ?:
TerminationChecker . . . December 14, 2018, at 04:35 PM by ?:
Modules . . . December 14, 2018, at 04:00 PM by ?:
PatternMatching . . . December 14, 2018, at 03:58 PM by ?:
Functions . . . December 14, 2018, at 03:57 PM by ?:
Postulates . . . December 14, 2018, at 03:56 PM by ?:
RecordsTutorial . . . December 14, 2018, at 03:56 PM by ?:
Records . . . December 14, 2018, at 03:55 PM by ?:
Data . . . December 14, 2018, at 03:52 PM by ?:
Declarations . . . December 14, 2018, at 03:51 PM by ?:
Pattern-matchingLambdas . . . December 14, 2018, at 03:49 PM by ?:
InstanceArguments . . . December 14, 2018, at 03:48 PM by ?:
ImplicitArguments . . . December 14, 2018, at 03:46 PM by ?:
FixityDeclarations . . . December 14, 2018, at 03:45 PM by ?:
Mixfix . . . December 14, 2018, at 03:44 PM by ?:
Layout . . . December 14, 2018, at 03:43 PM by ?:
Keywords . . . December 14, 2018, at 03:42 PM by ?:
Names . . . December 14, 2018, at 03:41 PM by ?:
Literals . . . December 14, 2018, at 03:40 PM by ?:
Comments . . . December 14, 2018, at 03:39 PM by ?:
SourceFiles . . . December 14, 2018, at 03:38 PM by ?:
TOC . . . January 22, 2018, at 03:17 PM by ASR: Removed broken items
LocalDefinitions . . . January 22, 2018, at 03:13 PM by ASR: Moved to Read the Docs
EmacsInterface . . . January 21, 2018, at 02:08 AM by ASR: Cleaning
The Agda Reference Manual . . . April 14, 2017, at 03:44 PM by ASR: Moved `Auto` documentation to the user manual
Pragmas . . . March 30, 2017, at 02:32 PM by ASR: Moved documentation of `--with-K` and `without-K` to the user manual
Core Syntax . . . January 17, 2017, at 03:23 PM by ASR: Removed incorrect documentation about forall
With-expression . . . February 17, 2016, at 09:42 AM by ?:
Pattern-matching Lambdas . . . January 08, 2016, at 05:15 PM by ?:
Foreign Function Interface . . . January 02, 2016, at 11:05 PM by ?:
Universe Polymorphism . . . September 15, 2015, at 10:07 PM by XIE Yuheng:
Modules . . . June 05, 2015, at 10:39 PM by kirstin: It's semicolons, not hyphens for multiple arguments to using
Compilation . . . December 23, 2014, at 09:35 PM by zachmoore99aTgmailpointcom: Removed random red links from code
Records Tutorial . . . December 17, 2014, at 07:11 PM by Twey: Add small section on recursive records, as the information is hard to find.
Functions . . . December 06, 2014, at 02:23 AM by Peter Selinger: \forall -> \all
Data . . . December 06, 2014, at 01:19 AM by Peter Selinger: Changed hyperlink for "universe"
Instance Arguments . . . December 05, 2014, at 05:07 PM by Peter Selinger: Added "forall"
Implicit Arguments . . . December 05, 2014, at 05:01 PM by Peter Selinger: Added "forall" synax for implicit arguments
Modelling Type Classes with Instance Arguments . . . December 04, 2014, at 07:25 PM by Peter Selinger: Attempting a redirect
Irrelevance . . . December 02, 2014, at 05:52 AM by Peter Selinger: Inserted TOC link
Totality . . . December 02, 2014, at 05:51 AM by Peter Selinger: Inserted TOC link
Reflection . . . December 02, 2014, at 05:51 AM by Peter Selinger: Inserted TOC link and grammar
Layout . . . December 02, 2014, at 04:48 AM by Peter Selinger: Added remark on exceptions
Postulates . . . December 02, 2014, at 04:17 AM by Peter Selinger: Typos
Declarations . . . December 02, 2014, at 02:24 AM by ?: Added fixity declarations
Fixity Declarations . . . December 02, 2014, at 02:23 AM by ?: Punctuation
Non-recursive Resolution for Instance Arguments . . . December 02, 2014, at 02:12 AM by ?: Inserted TOC link
Mixfix . . . December 02, 2014, at 01:12 AM by ?: Fixed typo "more than one name part". E.g. _x, x_, _x_ all have only one name part.
Bad in Haskell . . . November 29, 2014, at 01:09 AM by ?: Make indentation consistent
Pattern Matching . . . October 10, 2014, at 03:26 PM by ?:
Literals . . . July 21, 2014, at 12:05 PM by ?: removed spam link
Keywords . . . February 07, 2014, at 04:51 PM by Andr�s Sicard-Ram�rez: Removed codata from keywords list
Raw Irrelevance . . . December 01, 2013, at 12:25 AM by wj: Page no longer needed.
Intro What . . . November 02, 2013, at 06:37 AM by FZ: typo
Termination Checker . . . September 11, 2013, at 01:56 PM by ?: Minor language fixes
Local Definitions . . . April 19, 2013, at 04:11 PM by Andr�s Sicard-Ram�rez: Fixed typos
Records . . . January 21, 2013, at 02:10 PM by gallais: fixing the general form of a record declaration to match actual implementation
Names . . . December 11, 2012, at 05:45 AM by Andres Sicard-Ram�rez: Fixed characters not allowed in a name part
Structure of an Agda Program . . . November 11, 2012, at 02:35 AM by ?:
Finding the Values of Implicit Arguments . . . November 07, 2012, at 12:10 PM by Andreas Abel:
Troubleshooting . . . October 10, 2012, at 04:59 PM by Daniel Gustafsson: Added a troubleshooting section for showing fixes to common problems.
Mutual . . . October 09, 2012, at 10:39 AM by ?:
Prop . . . October 09, 2012, at 10:05 AM by ?:
Typing Rules . . . October 09, 2012, at 10:04 AM by ?:
Modules-Talk . . . June 21, 2012, at 02:57 AM by Anonymous:
Source Files . . . February 27, 2012, at 03:19 AM by Neil Strickland: various additional comments
Standard Library . . . February 25, 2012, at 10:09 PM by xz:
Emacs Interface . . . February 25, 2012, at 06:49 PM by xz:
Comments . . . February 24, 2012, at 02:49 PM by ?:
TOC . . . February 24, 2012, at 02:46 PM by ?:
Inductive Data Types and Pattern Matching . . . February 24, 2012, at 02:45 PM by ?:
Compiler . . . February 21, 2012, at 04:30 PM by xz:
Pattern Matching Lambdas . . . February 20, 2012, at 06:04 PM by ?:
Modelling Type Classes with Instance Arguments-Talk . . . January 31, 2012, at 12:07 AM by erus: !
Simple Inductive Types . . . December 08, 2011, at 05:53 PM by Wojciech Jedynak: Add a link
Non-recursive Resolution for Non-canonical Implicit Arguments . . . April 21, 2011, at 03:14 PM by Dominique Devriese: First version
Modelling Type Classes with Non-canonical Implicits . . . April 21, 2011, at 02:55 PM by Dominique Devriese: More details for ModellingTypeClassesWithNon-canonicalImplicits
Non-canonical Implicit Arguments . . . April 21, 2011, at 02:26 PM by Dominique Devriese: First version
Coinductive data types . . . January 01, 2011, at 01:44 PM by NAD: Linked to message describing some limitations of the current implementation.
Records-Talk . . . November 02, 2010, at 01:58 AM by Rob Simmons: sign
Lexical Matters . . . December 03, 2009, at 03:16 PM by NAD: Added some reserved words.
Functions-Talk . . . November 28, 2009, at 02:22 AM by Wolfram Kahl: Elementary questions about type syntax.
Implicit Arg . . . October 07, 2009, at 11:00 AM by NAD: Pointed out that the documentation does not match the implementation.
Parameterized Inductive Types . . . March 18, 2009, at 02:54 PM by Sigurd Meldgaard: singularized a word
Emacs . . . January 25, 2009, at 12:55 AM by ?: fix links
Literate Agda . . . December 01, 2008, at 06:17 AM by ?:
Codatatypes . . . August 27, 2008, at 04:09 PM by ?: typo
Emacs-Talk . . . June 04, 2008, at 04:56 PM by Miguel:
Emacs Mode Key Combinations . . . June 04, 2008, at 03:20 PM by NAD: There is no longer any special support for undo.
Local Def . . . June 04, 2008, at 01:39 PM by Ana Bove:
How to See Unicode in Emacs . . . June 04, 2008, at 10:34 AM by Bengt:
How to See Unicode in Emacs . . . June 04, 2008, at 10:25 AM by Bengt:
Bibliography . . . June 04, 2008, at 10:18 AM by Pierre:
Datatypes . . . June 03, 2008, at 03:55 PM by ?:
Overview . . . June 03, 2008, at 10:09 AM by Pierre:

Edit | History | Recent Changes (all) | Search

Page last modified on July 03, 2020, at 08:35 am