How to Install and Uninstall metamath-data Package on openSUSE Leap

Last updated: December 27,2024

Deprecated! Installation of this package may no longer be supported.

1. Install "metamath-data" package

Please follow the guidance below to install metamath-data on openSUSE Leap


    
        
            $
        

        
            
                sudo zypper refresh
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo zypper install
            
                        
                metamath-data
            
                    
    
    Copied

2. Uninstall "metamath-data" package

In this section, we are going to explain the necessary steps to uninstall metamath-data on openSUSE Leap:


    
        
            $
        

        
            
                sudo zypper remove
            
                        
                metamath-data
            
                    
    
    Copied

3. Information about the metamath-data package on openSUSE Leap

Information for package metamath-data:
--------------------------------------
Repository : Main Repository
Name : metamath-data
Version : 0.196-bp153.2.1
Arch : noarch
Vendor : openSUSE
Installed Size : 40,0 MiB
Installed : No
Status : not installed
Source package : metamath-0.196-bp153.2.1.src
Summary : Data base files for metamath
Description :
This package contains Metamath data base files for several formal theories.
* set.mm – Logic and set theory database (see Ch. 3 of the Metamath book).
* nf.mm – Logic and set theory database for Quine's New Foundations set theory.
* hol.mm – Higher order logic (simple type theory) database.
* iset.mm – Intuitionistic logic database.
* ql.mm – Quantum logic database.
* demo0.mm – Demo of simple formal system (see Ch. 2 of the Metamath book).
* miu.mm – Hofstadter's MIU-system (see Appendix D of the Metamath book).
* big-unifier.mm – A unification stress test (see comments in the file).
* peano.mm – A presentation of Peano arithmetic by Robert Solovay.