 In fact has the type codice_22 thus Metamath has to check that is also typed codice_22.The Metamath program is the original program created to manipulate databases written using the Metamath language.It has a text (command line) interface and is written in C. It can read a Metamath database into memory, verify the proofs of a database, modify the database (in particular by adding proofs), and write them back out to storage.