How to Install and Uninstall elpa-agda2-mode Package on Ubuntu 21.04 (Hirsute Hippo)

Last updated: May 17,2024

1. Install "elpa-agda2-mode" package

Here is a brief guide to show you how to install elpa-agda2-mode on Ubuntu 21.04 (Hirsute Hippo)

$ sudo apt update $ sudo apt install elpa-agda2-mode

2. Uninstall "elpa-agda2-mode" package

Please follow the step by step instructions below to uninstall elpa-agda2-mode on Ubuntu 21.04 (Hirsute Hippo):

$ sudo apt remove elpa-agda2-mode $ sudo apt autoclean && sudo apt autoremove

3. Information about the elpa-agda2-mode package on Ubuntu 21.04 (Hirsute Hippo)

Package: elpa-agda2-mode
Architecture: all
Version: 2.6.1-1build2
Priority: extra
Section: universe/editors
Source: agda
Origin: Ubuntu
Maintainer: Ubuntu Developers
Original-Maintainer: Debian Haskell Group
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Installed-Size: 208
Depends: agda-bin (<< 2.6.1-1build2.1~), agda-bin (>= 2.6.1-1build2), libghc-agda-dev (<< 2.6.1-1build2.1~), libghc-agda-dev (>= 2.6.1-1build2), dh-elpa-helper, emacsen-common
Recommends: emacs (>= 46.0)
Enhances: emacs, emacs24
Filename: pool/universe/a/agda/elpa-agda2-mode_2.6.1-1build2_all.deb
Size: 42324
MD5sum: 6d8d5e11230cd5c8a671cdb5250c52cc
SHA1: 8d0282eb87274894c9e7dbf15dc74da6bcc314bd
SHA256: b51a03cbc6bbd9611fb679cdaea140724768fd2a31d073bb98f61181f3f907c3
SHA512: 663b60be9a79385ca6e0d18a0d9eb01f1b341411f3f3c4409f4288ad04fce4e408930831d93cffd4292b003ed72d94ef857ea1071bc2065e027312b24a9620ad
Homepage: https://wiki.portal.chalmers.se/agda/
Description-en: dependently typed functional programming language — emacs mode
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 package contains the emacs interactive development mode for Agda. This
mode is the preferred way to write Agda code, and offers features such as
iterative development, refinement, case analysis and so on.
Description-md5: 7cfcb4a5e7415e1476d23d2fd002910b