]> matita.cs.unibo.it Git - helm.git/commit
Coercions are now generalized to the general form
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Aug 2007 13:36:44 +0000 (13:36 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Aug 2007 13:36:44 +0000 (13:36 +0000)
commit5da42f6120f3075c3da8ab3082ead39ea57955fa
tree052f3ee2f12304bc03dd853e57cc4dca63eb1ff2
parentf6bf40d380bdb66e1cb3315edebb3d276ba7a125
Coercions are now generalized to the general form
f: \forall xs:Ts. \forall a:A xs. \forall ys:Ts'. B xs a ys
where f is declared as a coercion from A ? to B ? ? ? using the syntax

   coercion uri arity saturations

where:
 1. arity and saturations are optional with default 0
 2. the saturations option is the number of ys

Useful example: it is now possible to declare a coercion from
 nat to \exists n:nat. 0 \leq n
obtaining something extremely close to Russel (the new implementation of
the Program tactic of Coq) up to the fact that coercions are not propagated
yet under mutcases and fixes.

TODO: composition of coercions having saturations <> 0 is not implemented
yet (but should be easy to do, at least on paper)
18 files changed:
helm/software/components/binaries/transcript/grafite.ml
helm/software/components/cic_unification/coercGraph.ml
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite/grafiteMarshal.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteSync.ml
helm/software/components/grafite_engine/grafiteSync.mli
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/library/cicCoercion.ml
helm/software/components/library/cicCoercion.mli
helm/software/components/library/coercDb.ml
helm/software/components/library/coercDb.mli
helm/software/components/library/librarySync.ml
helm/software/components/library/librarySync.mli
helm/software/components/tactics/closeCoercionGraph.ml
helm/software/components/tactics/closeCoercionGraph.mli
helm/software/matita/matita.ml