X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ffr2_map.ma;h=77a1c518a2d8dd6de8edd799dac8c13df36a8d5b;hb=8f1a123e61ff079b1f9ad63cc915470ec7e6abf3;hp=3de9abeb3e22fe3fb3adb08f1cea561f949ddcba;hpb=55c768d7e45babb300b5010463ba3196a68f1bbe;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma index 3de9abeb3..77a1c518a 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "ground/notation/functions/diamond_0.ma". -include "ground/notation/functions/semicolon_3.ma". +include "ground/notation/functions/element_e_0.ma". +include "ground/notation/functions/black_halfcircleright_3.ma". include "ground/arith/nat.ma". (* FINITE RELOCATION MAPS WITH PAIRS ****************************************) @@ -21,14 +21,15 @@ include "ground/arith/nat.ma". (*** mr2 *) inductive fr2_map: Type[0] := (*** nil2 *) - | fr2_nil : fr2_map +| fr2_empty: fr2_map (*** cons2 *) - | fr2_cons: nat → nat → fr2_map → fr2_map. +| fr2_lcons: nat → nat → fr2_map → fr2_map +. interpretation - "nil (finite relocation maps with pairs)" - 'Diamond = (fr2_nil). + "empty (finite relocation maps with pairs)" + 'ElementE = (fr2_empty). interpretation - "cons (finite relocation maps with pairs)" - 'Semicolon d h f = (fr2_cons d h f). + "left cons (finite relocation maps with pairs)" + 'BlackHalfCircleRight d h f = (fr2_lcons d h f).