How to Install and Uninstall agda Package on Ubuntu 16.04 LTS (Xenial Xerus)
Last updated: December 23,2024
1. Install "agda" package
This tutorial shows how to install agda on Ubuntu 16.04 LTS (Xenial Xerus)
$
sudo apt update
Copied
$
sudo apt install
agda
Copied
2. Uninstall "agda" package
Please follow the steps below to uninstall agda on Ubuntu 16.04 LTS (Xenial Xerus):
$
sudo apt remove
agda
Copied
$
sudo apt autoclean && sudo apt autoremove
Copied
3. Information about the agda package on Ubuntu 16.04 LTS (Xenial Xerus)
Package: agda
Priority: extra
Section: universe/misc
Installed-Size: 70
Maintainer: Ubuntu Developers
Original-Maintainer: Debian Haskell Group
Architecture: all
Version: 2.4.2.5-1build1
Depends: libghc-agda-dev, agda-bin, agda-mode, agda-stdlib, agda-stdlib-doc
Filename: pool/universe/a/agda/agda_2.4.2.5-1build1_all.deb
Size: 2966
MD5sum: 73c11592175d460b0202b9ea300eb091
SHA1: a0203f5e13a02899c5d626dfa0533fffc2e6e879
SHA256: 001126037a4963fb0df6bfcc471a0cd42acfdf6f7063d1f28c811b811ac81c94
Description-en: dependently typed functional programming language
Agda is a dependently typed functional programming language: It has inductive
families, which are like Haskell's GADTs, but they can be indexed by values and
not just types. It also has parameterised modules, mixfix operators, Unicode
characters, and an interactive Emacs interface (the type checker can assist in
the development of your code).
.
Agda is also a proof assistant: It is an interactive system for writing and
checking proofs. Agda is based on intuitionistic type theory, a foundational
system for constructive mathematics developed by the Swedish logician Per
Martin-Löf. It has many similarities with other proof assistants based on
dependent types, such as Coq, Epigram and NuPRL.
.
This is a meta package which provides Agda's emacs mode, executable, standard
library and its documentation.
Description-md5: 65333dc4f3e4d00a90419d96d9785d24
Homepage: http://wiki.portal.chalmers.se/agda/
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Origin: Ubuntu
Priority: extra
Section: universe/misc
Installed-Size: 70
Maintainer: Ubuntu Developers
Original-Maintainer: Debian Haskell Group
Architecture: all
Version: 2.4.2.5-1build1
Depends: libghc-agda-dev, agda-bin, agda-mode, agda-stdlib, agda-stdlib-doc
Filename: pool/universe/a/agda/agda_2.4.2.5-1build1_all.deb
Size: 2966
MD5sum: 73c11592175d460b0202b9ea300eb091
SHA1: a0203f5e13a02899c5d626dfa0533fffc2e6e879
SHA256: 001126037a4963fb0df6bfcc471a0cd42acfdf6f7063d1f28c811b811ac81c94
Description-en: dependently typed functional programming language
Agda is a dependently typed functional programming language: It has inductive
families, which are like Haskell's GADTs, but they can be indexed by values and
not just types. It also has parameterised modules, mixfix operators, Unicode
characters, and an interactive Emacs interface (the type checker can assist in
the development of your code).
.
Agda is also a proof assistant: It is an interactive system for writing and
checking proofs. Agda is based on intuitionistic type theory, a foundational
system for constructive mathematics developed by the Swedish logician Per
Martin-Löf. It has many similarities with other proof assistants based on
dependent types, such as Coq, Epigram and NuPRL.
.
This is a meta package which provides Agda's emacs mode, executable, standard
library and its documentation.
Description-md5: 65333dc4f3e4d00a90419d96d9785d24
Homepage: http://wiki.portal.chalmers.se/agda/
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Origin: Ubuntu