How to Install and Uninstall agda Package on Ubuntu 21.10 (Impish Indri)

Last updated: February 02,2025

1. Install "agda" package

Please follow the instructions below to install agda on Ubuntu 21.10 (Impish Indri)


    
        
            $
        

        
            
                sudo apt update
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt install
            
                        
                agda
            
                    
    
    Copied

2. Uninstall "agda" package

This is a short guide on how to uninstall agda on Ubuntu 21.10 (Impish Indri):


    
        
            $
        

        
            
                sudo apt remove
            
                        
                agda
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt autoclean && sudo apt autoremove
            
                    
    
    Copied

3. Information about the agda package on Ubuntu 21.10 (Impish Indri)

Package: agda
Architecture: all
Version: 2.6.1-1build2.1
Priority: extra
Section: universe/misc
Origin: Ubuntu
Maintainer: Ubuntu Developers
Original-Maintainer: Debian Haskell Group
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Installed-Size: 24
Depends: agda-bin, agda-stdlib, agda-stdlib-doc, elpa-agda2-mode, libghc-agda-dev
Filename: pool/universe/a/agda/agda_2.6.1-1build2.1_all.deb
Size: 4134
MD5sum: 60a286271ee8bceed8d6930ea7990f54
SHA1: 05f495490b50a10c75a8338915d6b614f10d261c
SHA256: ab255620b321a80cd5e7e1076ca5062b7448f29a93c6b52ed4350dfeebe5786c
SHA512: 35ecb43e62e178f27f5279cae59ba136abbf46fd3ec9a697857b6c50098d5dee8122f627a0bc4178bebe27b9779625dbe2ce8057b497df074c0ea5f50a18098a
Homepage: https://wiki.portal.chalmers.se/agda/
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