Meta Dedukti

1 What is Meta Dedukti?

Meta Dedukti is a tool for transforming a Dedukti file into another Dedukti file in which all terms have been normalized with respect to the current rewrite system.

2 Get Meta Dedukti

Meta Dedukti source code is distributed as a branch of Dedukti. It can also be installed using the Opam Package Manager.

$ opam repository add deducteam git://scm.gforge.inria.fr/opam-deducteam/opam-deducteam.git
$ opam update
$ opam install meta_dedukti

3 Usage

Meta Dedukti is invoked by the command dkmeta accepting the same arguments as Dedukti type-checker dkcheck. Meta Dedukti files typically have the extension .dkm. They can be converted to Dedukti .dk files by the following command:

$ dkmeta my_file.dkm > my_file.dk
logo inrialogo deducteam