This is a small human-written Dedukti library. It contains some definitions of simple datatypes and logical constructs.
Dependencies
GNU Make
Dedukti: versions 2.4 and 2.5 have been tested, for version 2.3.1 use the =v2.3.1= branch
(Optional) CSI^HO higher-order confluence checker: version 0.1.1 has been tested
Usage
To compile all the files, invoke =make=.
Dedukti has no default load path so it is not very useful to install the compiled =.dko= files system wide. To copy the compiled file to some place =
cp -t
To check for confluence, invoke
make CSIHO_PATH=
where =
Please note that the experimental files =dk_monads.dk= and =dk_monads_coc.dk= are purposely not confluent
The library contains the following files:
| File | Description | Operations | |------------------+---------------------------------------+-------------------------------------------------------------------------------------------------------------------| | =cc= | Encoding of polymorphism | Polymorphic product and arrow types | | =dk_type= | Basic type constructions | Cartesian product, Sigma-types, Sum-types | | =dk_bool= | Booleans | dependent pattern-matching, alternative, logical connectives | | =dk_list= | Polymorphic lists | dependent pattern-matching, concatenation, map | | =dk_nat= | Peano (unary) natural numbers | ordering, equality, addition, multiplication, min, max, division, exponentiation, conversion from lists of digits | | =dk_int= | Unary integers from smart constructor | abs, ordering, equality, addition, multiplication, opposite, subtraction, min, max, division | | =dk_machine_int= | N-bits machine integers | same as dk_int + signed and unsigned orderings, conversion from unary | | =dk_binary_nat= | Same but not dependent | same as dk_int + conversion to machine_int | | =dk_char= | Chars are 7-bits integers | equality, representations for digits and letters | | =dk_string= | Strings are lists of chars | | | =dk_opt= | Polymorphic option type | | | =dk_fail= | | =dk_fail.fail : A : cc.uT -> cc.eT A= | | =dk_logic= | Impredicative Prop : type | intuitionistic logical connectives, reasoning on booleans and equality |
Obsolete | File | Description | |---------------+---------------------------------------------------------------------------+ | =dk_tuple= | Use dk_type instead | | =dk_builtins= | Basic types for the translation of FoCaLiZe standard library into Dedukti |
Experimental | File | Description | |-----------------+---------------------------------------------------------------------------| | =slist= | Lists of natural numbers sorted by construction | | =dk_monads= | Monadic laws enforced by rewriting (non-linear) | | =dk_monads_coc= | Going further by not encoding polymorphism (non-linear and requires -coc) |