How to Install and Uninstall libcoq-mathcomp-character Package on Kali Linux

Last updated: January 10,2025

1. Install "libcoq-mathcomp-character" package

Please follow the guidance below to install libcoq-mathcomp-character on Kali Linux

$ sudo apt update $ sudo apt install libcoq-mathcomp-character

2. Uninstall "libcoq-mathcomp-character" package

In this section, we are going to explain the necessary steps to uninstall libcoq-mathcomp-character on Kali Linux:

$ sudo apt remove libcoq-mathcomp-character $ sudo apt autoclean && sudo apt autoremove

3. Information about the libcoq-mathcomp-character package on Kali Linux

Package: libcoq-mathcomp-character
Source: ssreflect (2.1.0-1)
Version: 2.1.0-1+b1
Installed-Size: 14019
Maintainer: Debian OCaml Maintainers
Architecture: amd64
Replaces: libssreflect-coq
Provides: libcoq-mathcomp-character-zazo6
Depends: libcoq-mathcomp-field (= 2.1.0-1+b1), libcoq-hierarchy-builder-qv203, libcoq-stdlib-6gs52
Breaks: libssreflect-coq (<= 2.1.0-1+b1)
Size: 3941680
SHA256: e5fdda18bc585c6c3e32d188de35a6046f84f8f2c9b89e31b0d8e6e275608356
SHA1: 142ccccd7600982d6a9be6ebc4254aa773d5eb1b
MD5sum: b3041a59e414a55ff51437b3d9a720ac
Description: Mathematical Components library for Coq (character)
The Mathematical Components Library is an extensive and coherent
repository of formalized mathematical theories. It is based on the
Coq proof assistant, powered with the Coq/SSReflect language.
.
These formal theories cover a wide spectrum of topics, ranging from
the formal theory of general-purpose data structures like lists,
prime numbers or finite graphs, to advanced topics in algebra.
.
The formalization technique adopted in the library, called "small
scale reflection", leverages the higher-order nature of Coq's
underlying logic to provide effective automation for many small,
clerical proof steps. This is often accomplished by restating
("reflecting") problems in a more concrete form, hence the name. For
example, arithmetic comparison is not an abstract predicate, but
rather a function computing a Boolean.
.
This package installs the character theory part of the library
(group representations, characters and class functions).
Description-md5:
Homepage: https://math-comp.github.io/math-comp/
Section: math
Priority: optional
Filename: pool/main/s/ssreflect/libcoq-mathcomp-character_2.1.0-1+b1_amd64.deb