How to Install and Uninstall coq-theories Package on Ubuntu 20.10 (Groovy Gorilla)

Last updated: May 16,2024

1. Install "coq-theories" package

Here is a brief guide to show you how to install coq-theories on Ubuntu 20.10 (Groovy Gorilla)


    
        
            $
        

        
            
                sudo apt update
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt install
            
                        
                coq-theories
            
                    
    
    Copied

2. Uninstall "coq-theories" package

This tutorial shows how to uninstall coq-theories on Ubuntu 20.10 (Groovy Gorilla):


    
        
            $
        

        
            
                sudo apt remove
            
                        
                coq-theories
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt autoclean && sudo apt autoremove
            
                    
    
    Copied

3. Information about the coq-theories package on Ubuntu 20.10 (Groovy Gorilla)

Package: coq-theories
Architecture: amd64
Version: 8.12.0-3build1
Priority: optional
Section: universe/math
Source: coq
Origin: Ubuntu
Maintainer: Ubuntu Developers
Original-Maintainer: Debian OCaml Maintainers
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Installed-Size: 285508
Depends: coq-8.12.0+4.08.1
Recommends: coq (>= 8.0)
Breaks: coq-doc (<= 8.0pl1.0-2), coq-libs (<< 8.2.pl1)
Replaces: coq-libs (<< 8.2.pl1)
Filename: pool/universe/c/coq/coq-theories_8.12.0-3build1_amd64.deb
Size: 36980788
MD5sum: 59f11180dad18b87de2d5220cdac0195
SHA1: 1b200532978b0eba1f18f38eb4119f703e8549d2
SHA256: f6a45312b5cff507852f946571a3e797b6705bd386f2d6dc6a1b36122bba10e0
SHA512: 4e76f8864d806fb5f0c9147be5fb97b73c99d0ac0fd17710da98f8acbe0b077c1a8accca609c1afa758ce37eac8b87366559dbb7fd125a39668d7fc3f94e53ad
Homepage: http://coq.inria.fr/
Description-en: proof assistant for higher-order logic (theories)
Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal
specification. It is developed using Objective Caml and Camlp5.
.
This package provides existing theories that new proofs can be
based upon, including theories of arithmetic and Boolean values.
Description-md5: 9e601d42ac375ebc4cb75dff6e4c368e