Agda User Manual
Open the PDF directly: View PDF .
Page Count: 157
|Open PDF In Browser||View PDF|
Agda User Manual Release 2.6.0 The Agda Team Oct 18, 2018 Contents 1 Overview 1 2 Getting Started 2.1 Prerequisites . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Installation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.3 Quick Guide to Editing, Type Checking and Compiling Agda Code . . . . . . . . . . . . . . . . . . 3 3 4 6 3 Language Reference 3.1 Abstract definitions . . . . . . . 3.2 Built-ins . . . . . . . . . . . . 3.3 Coinduction . . . . . . . . . . 3.4 Copatterns . . . . . . . . . . . 3.5 Core language . . . . . . . . . 3.6 Cubical Type Theory in Agda . 3.7 Data Types . . . . . . . . . . . 3.8 Foreign Function Interface . . . 3.9 Function Definitions . . . . . . 3.10 Function Types . . . . . . . . . 3.11 Implicit Arguments . . . . . . . 3.12 Instance Arguments . . . . . . 3.13 Irrelevance . . . . . . . . . . . 3.14 Lambda Abstraction . . . . . . 3.15 Local Definitions: let and where 3.16 Lexical Structure . . . . . . . . 3.17 Literal Overloading . . . . . . 3.18 Mixfix Operators . . . . . . . . 3.19 Module System . . . . . . . . . 3.20 Mutual Recursion . . . . . . . 3.21 Pattern Synonyms . . . . . . . 3.22 Positivity Checking . . . . . . . 3.23 Postulates . . . . . . . . . . . . 3.24 Pragmas . . . . . . . . . . . . 3.25 Record Types . . . . . . . . . . 3.26 Reflection . . . . . . . . . . . . 3.27 Rewriting . . . . . . . . . . . . 3.28 Safe Agda . . . . . . . . . . . 3.29 Sized Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 9 12 22 24 27 27 28 31 36 39 40 42 47 52 53 57 60 62 64 69 70 71 73 74 75 82 90 90 91 i 4 3.30 3.31 3.32 3.33 3.34 3.35 3.36 Syntactic Sugar . . . . Syntax Declarations . Telescopes . . . . . . Termination Checking Universe Levels . . . With-Abstraction . . . Without K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 . 98 . 99 . 99 . 100 . 100 . 110 Tools 4.1 4.2 4.3 4.4 4.5 4.6 4.7 4.8 Automatic Proof Search (Auto) Command-line options . . . . . Compilers . . . . . . . . . . . Emacs Mode . . . . . . . . . . Literate Programming . . . . . Generating HTML . . . . . . . Generating LaTeX . . . . . . . Library Management . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 113 116 121 123 127 129 129 140 5 Contribute 143 5.1 Documentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143 6 The Agda License 147 7 The Agda Team 149 8 Indices and tables 151 Bibliography ii 153 CHAPTER 1 Overview Note: The Agda User Manual is a work-in-progress and is still incomplete. Contributions, additions and corrections to the Agda manual are greatly appreciated. To do so, please open a pull request or issue on the Github Agda page. This is the manual for the Agda programming language, its type checking, compilation and editing system and related tools. A description of the Agda language is given in chapter Language Reference. Guidance on how the Agda editing and compilation system can be used can be found in chapter Tools. 1 Agda User Manual, Release 2.6.0 2 Chapter 1. Overview CHAPTER 2 Getting Started 2.1 Prerequisites You need recent versions of the following programs to compile Agda: • GHC: https://www.haskell.org/ghc/ • cabal-install: https://www.haskell.org/cabal/ • Alex: https://www.haskell.org/alex/ • Happy: https://www.haskell.org/happy/ • GNU Emacs: http://www.gnu.org/software/emacs/ You should also make sure that programs installed by cabal-install are on your shell’s search path. For instructions on installing a suitable version of Emacs under Windows, see Installing Emacs under Windows. Non-Windows users need to ensure that the development files for the C libraries zlib* and ncurses* are installed (see http://zlib.net and http://www.gnu.org/software/ncurses/). Your package manager may be able to install these files for you. For instance, on Debian or Ubuntu it should suffice to run apt-get install zlib1g-dev libncurses5-dev as root to get the correct files installed. Optionally one can also install the ICU library, which is used to implement the --count-clusters flag. Under Debian or Ubuntu it may suffice to install libicu-dev. Once the ICU library is installed one can hopefully enable the --count-clusters flag by giving the -fenable-cluster-counting flag to cabal install. 2.1.1 Installing Emacs under Windows A precompiled version of Emacs 24.3, with the necessary mathematical fonts, is available at http://homepage.cs.uiowa. edu/~astump/agda/ . 3 Agda User Manual, Release 2.6.0 2.2 Installation There are several ways to install Agda: • Using a released source package from Hackage • Using a binary package prepared for your platform • Using the development version from the Git repository Agda can be installed using different flags (see Installation Flags). 2.2.1 Installation from Hackage You can install the latest released version of Agda from Hackage. Install the prerequisites and then run the following commands: cabal update cabal install Agda agda-mode setup The last command tries to set up Emacs for use with Agda via the Emacs mode. As an alternative you can copy the following text to your .emacs file: (load-file (let ((coding-system-for-read 'utf-8)) (shell-command-to-string "agda-mode locate"))) It is also possible (but not necessary) to compile the Emacs mode’s files: agda-mode compile This can, in some cases, give a noticeable speedup. Warning: If you reinstall the Agda mode without recompiling the Emacs Lisp files, then Emacs may continue using the old, compiled files. 2.2.2 Prebuilt Packages and System-Specific Instructions Arch Linux The following prebuilt packages are available: • Agda • Agda standard library Debian / Ubuntu Prebuilt packages are available for Debian testing/unstable and Ubuntu from Karmic onwards. To install: apt-get install agda-mode This should install Agda and the Emacs mode. The standard library is available in Debian testing/unstable and Ubuntu from Lucid onwards. To install: 4 Chapter 2. Getting Started Agda User Manual, Release 2.6.0 apt-get install agda-stdlib More information: • Agda (Debian) • Agda standard library (Debian) • Agda (Ubuntu) • Agda standard library (Ubuntu) Reporting bugs: Please report any bugs to Debian, using: reportbug -B debian agda reportbug -B debian agda-stdlib Fedora Agda is packaged in Fedora (since before Fedora 18). yum install Agda will pull in emacs-agda-mode and ghc-Agda-devel. FreBSD Packages are available from FreshPorts for Agda and Agda standard library. NixOS Agda is part of the Nixpkgs collection that is used by https://nixos.org/nixos. To install Agda and agda-mode for Emacs, type: nix-env -f "
Source Exif Data:
File Type : PDF File Type Extension : pdf MIME Type : application/pdf PDF Version : 1.5 Linearized : No Page Count : 157 Page Mode : UseOutlines Author : The Agda Team Title : Agda User Manual Subject : Creator : LaTeX with hyperref package Producer : pdfTeX-1.40.16 Create Date : 2018:10:18 16:33:29Z Modify Date : 2018:10:18 16:33:29Z Trapped : False PTEX Fullbanner : This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) kpathsea version 6.2.1EXIF Metadata provided by EXIF.tools