matita/components/binaries/matex/test/basic_1.conf.xml

   1 <?xml version="1.0" encoding="utf-8"?>
   2 <helm_registry>
   3   <section name="devel">
   4     <key name="basic1">matita.lambdadelta.basic_1</key>
   5   </section>
   6   <section name="matex.alpha">
   7     <key name="type">$(devel.basic1).T.defs.B.B.type b I</key>
   8     <key name="type">$(devel.basic1).T.defs.B.B.type ee I</key>
   9     <key name="type">$(devel.basic1).T.defs.B.B.type x I</key>
  10
  11     <key name="type">$(devel.basic1).T.defs.F.F.type ee I</key>
  12     <key name="type">$(devel.basic1).T.defs.F.F.type f I</key>
  13     <key name="type">$(devel.basic1).T.defs.F.F.type x I</key>
  14
  15     <key name="type">$(devel.basic1).T.defs.K.K.type e I</key>
  16     <key name="type">$(devel.basic1).T.defs.K.K.type ee I</key>
  17     <key name="type">$(devel.basic1).T.defs.K.K.type k I</key>
  18     <key name="type">$(devel.basic1).T.defs.K.K.type h I</key>
  19     <key name="type">$(devel.basic1).T.defs.K.K.type x I</key>
  20
  21     <key name="type">$(devel.basic1).C.defs.C.C.type _ X</key>
  22     <key name="type">$(devel.basic1).C.defs.C.C.type a X</key>
  23     <key name="type">$(devel.basic1).C.defs.C.C.type c L</key>
  24     <key name="type">$(devel.basic1).C.defs.C.C.type d L</key>
  25     <key name="type">$(devel.basic1).C.defs.C.C.type e K</key>
  26     <key name="type">$(devel.basic1).C.defs.C.C.type ee X</key>
  27     <key name="type">$(devel.basic1).C.defs.C.C.type x X</key>
  28     <key name="type">$(devel.basic1).C.defs.C.C.type y Y</key>
  29
  30     <key name="type">$(devel.basic1).T.defs.T.T.type _ X</key>
  31     <key name="type">$(devel.basic1).T.defs.T.T.type e X</key>
  32     <key name="type">$(devel.basic1).T.defs.T.T.type ee X</key>
  33     <key name="type">$(devel.basic1).T.defs.T.T.type t T</key>
  34     <key name="type">$(devel.basic1).T.defs.T.T.type u U</key>
  35     <key name="type">$(devel.basic1).T.defs.T.T.type v V</key>
  36     <key name="type">$(devel.basic1).T.defs.T.T.type w W</key>
  37     <key name="type">$(devel.basic1).T.defs.T.T.type wi W</key>
  38     <key name="type">$(devel.basic1).T.defs.T.T.type x X</key>
  39     <key name="type">$(devel.basic1).T.defs.T.T.type y Y</key>
  40     <key name="type">$(devel.basic1).T.defs.T.T.type z Z</key>
  41
  42     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type _ Xs</key>
  43     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type e Xs</key>
  44     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type ee Xs</key>
  45     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type t Ts</key>
  46     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type ts Ts</key>
  47     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type ul Us</key>
  48     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type us Us</key>
  49     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type vs Vs</key>
  50     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type ws Ws</key>
  51     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type xs Xs</key>
  52     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type x Xs</key>
  53     <key name="type">$(devel.basic1).tlist.defs.TList.TList.type y Ys</key>
  54
  55     <key name="type">$(devel.basic1).A.defs.A.A.type _ X</key>
  56     <key name="type">$(devel.basic1).A.defs.A.A.type a A</key>
  57     <key name="type">$(devel.basic1).A.defs.A.A.type b B</key>
  58     <key name="type">$(devel.basic1).A.defs.A.A.type e X</key>
  59     <key name="type">$(devel.basic1).A.defs.A.A.type ee X</key>
  60     <key name="type">$(devel.basic1).A.defs.A.A.type l X</key>
  61     <key name="type">$(devel.basic1).A.defs.A.A.type x X</key>
  62     <key name="type">$(devel.basic1).A.defs.A.A.type y Y</key>
  63
  64     <key name="type">$(devel.basic1).G.defs.G.G.type g h</key>
  65
  66     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type _ x</key>
  67     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type d' d</key>
  68     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type d d</key>
  69     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type e e</key>
  70     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type ee e</key>
  71     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type f f</key>
  72     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type g g</key>
  73     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type h h</key>
  74     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type i i</key>
  75     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type j j</key>
  76     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type k k</key>
  77     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type l l</key>
  78     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type m m</key>
  79     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type n n</key>
  80     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type next f</key>
  81     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type v v</key>
  82     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type w w</key>
  83     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type x x</key>
  84     <key name="type">$(devel.legacy1).coq.defs.nat.nat.type y y</key>
  85
  86     <key name="type">$(devel.legacy1).coq.defs.bool.bool.type b b</key>
  87     <key name="type">$(devel.legacy1).coq.defs.bool.bool.type x x</key>
  88
  89     <key name="type">$(devel.ground1).plist.defs.PList.PList.type _ f</key>
  90     <key name="type">$(devel.ground1).plist.defs.PList.PList.type e f</key>
  91     <key name="type">$(devel.ground1).plist.defs.PList.PList.type ee f</key>
  92     <key name="type">$(devel.ground1).plist.defs.PList.PList.type hds f</key>
  93     <key name="type">$(devel.ground1).plist.defs.PList.PList.type is f</key>
  94     <key name="type">$(devel.ground1).plist.defs.PList.PList.type p f</key>
  95     <key name="type">$(devel.ground1).plist.defs.PList.PList.type q f</key>
  96     <key name="type">$(devel.ground1).plist.defs.PList.PList.type y f</key>
  97
  98     <key name="type">Prop P R</key>
  99     <key name="type">Prop Q R</key>
 100
 101     <key name="type">Type[cic:/matita/pts/Type0.univ] P S</key>
 102
 103     <key name="sort">Prop H H</key>
 104     <key name="sort">Prop Hle H</key>
 105     <key name="sort">Prop IH IH</key>
 106     <key name="sort">Prop IHc IH</key>
 107     <key name="sort">Prop IHd IH</key>
 108     <key name="sort">Prop IHe IH</key>
 109     <key name="sort">Prop IHh IH</key>
 110     <key name="sort">Prop IHi IH</key>
 111     <key name="sort">Prop IHj IH</key>
 112     <key name="sort">Prop IHn IH</key>
 113     <key name="sort">Prop IHx IH</key>
 114     <key name="sort">Prop a H</key>
 115     <key name="sort">Prop c H</key>
 116     <key name="sort">Prop d H</key>
 117     <key name="sort">Prop e H</key>
 118     <key name="sort">Prop f H</key>
 119     <key name="sort">Prop g H</key>
 120     <key name="sort">Prop h H</key>
 121     <key name="sort">Prop i H</key>
 122     <key name="sort">Prop l H</key>
 123     <key name="sort">Prop n H</key>
 124     <key name="sort">Prop p H</key>
 125     <key name="sort">Prop s H</key>
 126     <key name="sort">Prop t H</key>
 127     <key name="sort">Prop w H</key>
 128     <key name="sort">Prop x H</key>
 129
 130     <key name="sort">Type[cic:/matita/pts/Type0.univ] f a</key>
 131
 132     <key name="gref">clt_wf__q_ind q_ind_aux</key>
 133
 134     <key name="gref">ex1__leq_sort_SS leq_sort_SS_aux</key>
 135
 136     <key name="gref">flt_wf__q_ind q_ind_aux</key>
 137
 138     <key name="gref">llt_wf__q_ind q_ind_aux</key>
 139
 140     <key name="gref">nf2_gen__nf2_gen_aux nf2_gen_aux</key>
 141
 142     <key name="gref">pc3_ind_left__pc3_left_pc3 pc3_left_pc3_aux</key>
 143     <key name="gref">pc3_ind_left__pc3_left_pr3 pc3_left_pr3_aux</key>
 144     <key name="gref">pc3_ind_left__pc3_left_sym pc3_left_sym_aux</key>
 145     <key name="gref">pc3_ind_left__pc3_left_trans pc3_left_trans_aux</key>
 146     <key name="gref">pc3_ind_left__pc3_pc3_left pc3_pc3_left_aux</key>
 147     <key name="gref">pc3_wcpr0__pc3_wcpr0_t_aux pc3_wcpr0_t_aux</key>
 148
 149     <key name="gref">pr0_confluence__pr0_cong_delta pr0_cong_delta_aux</key>
 150     <key name="gref">pr0_confluence__pr0_cong_upsilon_cong pr0_cong_upsilon_cong_aux</key>
 151     <key name="gref">pr0_confluence__pr0_cong_upsilon_delta pr0_cong_upsilon_delta_aux</key>
 152     <key name="gref">pr0_confluence__pr0_cong_upsilon_refl pr0_cong_upsilon_refl_aux</key>
 153     <key name="gref">pr0_confluence__pr0_cong_upsilon_zeta pr0_cong_upsilon_zeta_aux</key>
 154     <key name="gref">pr0_confluence__pr0_delta_delta pr0_delta_delta_aux</key>
 155     <key name="gref">pr0_confluence__pr0_delta_tau pr0_delta_tau_aux</key>
 156     <key name="gref">pr0_confluence__pr0_upsilon_upsilon pr0_upsilon_upsilon_aux</key>
 157
 158     <key name="gref">pr2_confluence__pr2_delta_delta pr2_delta_delta_aux</key>
 159     <key name="gref">pr2_confluence__pr2_free_delta pr2_free_delta_aux</key>
 160     <key name="gref">pr2_confluence__pr2_free_free pr2_free_free_aux</key>
 161
 162     <key name="gref">sc3_props__sc3_sn3_abst sc3_sn3_abst_aux</key>
 163
 164     <key name="gref">terms_props__bind_dec bind_dec_aux</key>
 165     <key name="gref">terms_props__flat_dec flat_dec_aux</key>
 166     <key name="gref">terms_props__kind_dec kind_dec_aux</key>
 167
 168     <key name="gref">tlt_wf__q_ind q_ind_aux</key>
 169     <key name="gref">tslt_wf__q_ind q_ind_aux</key>
 170     <key name="gref">ty3_nf2_gen__ty3_nf2_inv_abst_aux ty3_nf2_inv_abst_aux</key>
 171   </section>
 172   <section name="matex.notation">
 173 <!--
 174 $(devel.basic1).A.defs.A.AHead.type 0</key>
 175 $(devel.basic1).A.defs.A.ASort.type 0</key>
 176 $(devel.basic1).A.fwd.A_rect.A_rect.type 0</key>
 177 $(devel.basic1).aplus.defs.aplus.aplus.type 0</key>
 178 $(devel.basic1).app.defs.app1.app1.type 0</key>
 179 $(devel.basic1).app.defs.cbk.cbk.type 0</key>
 180 $(devel.basic1).aprem.defs.aprem.aprem.type 0</key>
 181 $(devel.basic1).arity.defs.arity.arity.type 0</key>
 182 $(devel.basic1).asucc.defs.asucc.asucc.type 0</key>
 183 $(devel.basic1).C.defs.C.CHead.type 0</key>
 184 $(devel.basic1).C.defs.C.CSort.type 0</key>
 185 $(devel.basic1).C.defs.cle.type 0</key>
 186 $(devel.basic1).C.defs.clt.type 0</key>
 187 $(devel.basic1).C.defs.CTail.CTail.type 0</key>
 188 $(devel.basic1).C.defs.cweight.cweight.type 0</key>
 189 $(devel.basic1).C.fwd.C_rect.C_rect.type 0</key>
 190 $(devel.basic1).cimp.defs.cimp.type 0</key>
 191 $(devel.basic1).clear.defs.clear.clear.type 0</key>
 192 $(devel.basic1).clen.defs.clen.clen.type 0</key>
 193 $(devel.basic1).cnt.defs.cnt.cnt.type 0</key>
 194 $(devel.basic1).csuba.defs.csuba.csuba.type 0</key>
 195 $(devel.basic1).csubc.defs.csubc.csubc.type 0</key>
 196 $(devel.basic1).csubst0.defs.csubst0.csubst0.type 0</key>
 197 $(devel.basic1).csubst1.defs.csubst1.csubst1.type 0</key>
 198 $(devel.basic1).csubt.defs.csubt.csubt.type 0</key>
 199 $(devel.basic1).csubv.defs.csubv.csubv.type 0</key>
 200 -->
 201     <key name="const">$(devel.basic1).drop1.defs.drop1.drop1.type DropS 2 0</key>
 202 <!--
 203 $(devel.basic1).drop1.defs.ptrans.ptrans.type 0</key>
 204 -->
 205     <key name="const">$(devel.basic1).drop.defs.drop.drop.type Drop 3 0</key>
 206 <!--
 207 $(devel.basic1).ex0.defs.leqz.leqz.type 0</key>
 208 $(devel.basic1).flt.defs.flt.type 0</key>
 209 $(devel.basic1).flt.defs.fweight.type 0</key>
 210 $(devel.basic1).fsubst0.defs.fsubst0.fsubst0.type 0</key>
 211 $(devel.basic1).G.defs.G.mk_G.type 0</key>
 212 $(devel.basic1).G.defs.next.next.type 0</key>
 213 $(devel.basic1).getl.defs.getl.getl.type 0</key>
 214 $(devel.basic1).iso.defs.iso.iso.type 0</key>
 215 $(devel.basic1).leq.defs.leq.leq.type 0</key>
 216 -->
 217     <key name="const">$(devel.basic1).lift1.defs.lift1.lift1.type FunLiftS 2 0</key>
 218     <key name="const">$(devel.basic1).lift1.defs.lifts1.lifts1.type FunLiftS 2 0</key>
 219 <!--
 220 $(devel.basic1).lift1.defs.trans.trans.type 0</key>
 221 -->
 222     <key name="const">$(devel.basic1).lift.defs.lifts.lifts.type FunLift 3 0</key>
 223     <key name="const">$(devel.basic1).lift.defs.lift.type FunLift 3 0</key>
 224 <!--
 225 $(devel.basic1).lift.defs.lref_map.lref_map.type 0</key>
 226 $(devel.basic1).llt.defs.llt.type 0</key>
 227 $(devel.basic1).llt.defs.lweight.lweight.type 0</key>
 228 $(devel.basic1).next_plus.defs.next_plus.next_plus.type 0</key>
 229 $(devel.basic1).nf2.defs.nf2.type 0</key>
 230 $(devel.basic1).nf2.defs.nfs2.nfs2.type 0</key>
 231 $(devel.basic1).pc1.defs.pc1.type 0</key>
 232 $(devel.basic1).pc3.defs.pc3_left.pc3_left.type 0</key>
 233 $(devel.basic1).pc3.defs.pc3.type 0</key>
 234 $(devel.basic1).pr0.defs.pr0.pr0.type 0</key>
 235 $(devel.basic1).pr1.defs.pr1.pr1.type 0</key>
 236 $(devel.basic1).pr2.defs.pr2.pr2.type 0</key>
 237 $(devel.basic1).pr3.defs.pr3.pr3.type 0</key>
 238 $(devel.basic1).r.defs.r.type 0</key>
 239 $(devel.basic1).sc3.defs.sc3.sc3.type 0</key>
 240 $(devel.basic1).s.defs.s.type 0</key>
 241 $(devel.basic1).sn3.defs.sn3.sn3.type 0</key>
 242 $(devel.basic1).sn3.defs.sns3.sns3.type 0</key>
 243 $(devel.basic1).sty0.defs.sty0.sty0.type 0</key>
 244 $(devel.basic1).sty1.defs.sty1.sty1.type 0</key>
 245 $(devel.basic1).subst0.defs.subst0.subst0.type 0</key>
 246 $(devel.basic1).subst1.defs.subst1.subst1.type 0</key>
 247 $(devel.basic1).subst.defs.subst.subst.type 0</key>
 248 $(devel.basic1).T.defs.K.Bind.type 0</key>
 249 $(devel.basic1).T.defs.K.Flat.type 0</key>
 250 $(devel.basic1).T.defs.tle.type 0</key>
 251 $(devel.basic1).T.defs.T.THead.type 0</key>
 252 $(devel.basic1).T.defs.T.TLRef.type 0</key>
 253 $(devel.basic1).T.defs.T.TSort.type 0</key>
 254 $(devel.basic1).T.defs.tweight.tweight.type 0</key>
 255 $(devel.basic1).T.fwd.T_rect.T_rect.type 0</key>
 256 -->
 257     <key name="const">$(devel.basic1).tlist.defs.TApp.TApp.type RevConsA 2 0</key>
 258 <!--
 259 $(devel.basic1).tlist.defs.THeads.THeads.type 0</key>
 260 -->
 261     <key name="const">$(devel.basic1).tlist.defs.TList.TCons.type ConsA 2 0</key>
 262 <!--
 263 $(devel.basic1).tlist.defs.tslen.tslen.type 0</key>
 264 $(devel.basic1).tlist.defs.tslt.type 0</key>
 265 $(devel.basic1).tlt.defs.tlt.type 0</key>
 266 $(devel.basic1).tlt.defs.wadd.type 0</key>
 267 $(devel.basic1).tlt.defs.weight_map.weight_map.type 0</key>
 268 $(devel.basic1).tlt.defs.weight.type 0</key>
 269 $(devel.basic1).ty3.defs.ty3.ty3.type 0</key>
 270 $(devel.basic1).ty3.defs.tys3.tys3.type 0</key>
 271 $(devel.basic1).ty3.nf2.ty3_nf2_inv_abst_premise.type 0</key>
 272 $(devel.basic1).wcpr0.defs.wcpr0.wcpr0.type 0</key>
 273 $(devel.basic1).wf3.defs.wf3.wf3.type 0</key>
 274 -->
 275   </section>
 276 </helm_registry>