]> matita.cs.unibo.it Git - helm.git/commit
updating the structures for sorts
authorFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Sat, 15 Jun 2019 13:19:59 +0000 (15:19 +0200)
committerFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Sat, 15 Jun 2019 13:19:59 +0000 (15:19 +0200)
commit647b419e96770d90a82d7a9e5e8843566a9f93ee
treeb7ace4e3b0518c8f0c27b424ff4e9e6929b26c53
parentf308429a0fde273605a2330efc63268b4ac36c99
updating the structures for sorts

+ strict monotonicity is now an optional property
+ new optional properties: acyclicity and decidability
+ "next" now has a specific notation
+ refactored sort degree is now based on acyclicity and decidability
20 files changed:
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma
matita/matita/contribs/lambdadelta/static_2/etc/sh_lt.etc
matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma
matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma
matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl