Tags

new file structure, splitted pcf-file

added more arithmetical operations

explicit definition of cupdate

reordered formulas

Removed ty_bool, f_bool and f_ite and defined them by the other constructors. The corresponding old f_deriv-rules were also prooven by the other rules. In addition, comoproj-v1.2.0 is now included

some renamings

added description, how you can compile your project in multiple versions. added latest as additional default version

replaced f_bool and f_ite by defining them via f_case. Effects on bigCBN/bigCBV missing. at some places, some subproofs are not already written down in PCF.v

added headlines for coqdoc to structure toc.html a bit more

Implemented coproducts and the maybe-monad, refactored some pieces of code

implemented de-bruijn-indices to pcf

maintained file structure, now the content is splitted in different files.

first version of mbprog-script, covering pcf-big-cbn/-cbv-strategies and example of faculty function