helm/software/matita/contribs/procedural/Coq/Coq.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "preamble.ma".
  18
  19 (* From Arith/Compare *****************************************************)
  20
  21 (* NOTATION
  22 Notation not_eq_sym := sym_not_eq.
  23 *)
  24
  25 (* From Bool/Bool *********************************************************)
  26
  27 (* NOTATION
  28 Infix "||" := orb (at level 50, left associativity) : bool_scope.
  29 *)
  30
  31 (* NOTATION
  32 Infix "&&" := andb (at level 40, left associativity) : bool_scope.
  33 *)
  34
  35 (* From Init/Datatypes ****************************************************)
  36
  37 (* NOTATION
  38 Add Printing If bool.
  39 *)
  40
  41 (* NOTATION
  42 Notation "x + y" := (sum x y) : type_scope.
  43 *)
  44
  45 (* NOTATION
  46 Add Printing Let prod.
  47 *)
  48
  49 (* NOTATION
  50 Notation "x * y" := (prod x y) : type_scope.
  51 *)
  52
  53 (* NOTATION
  54 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
  55 *)
  56
  57 (* From Init/Logic ********************************************************)
  58
  59 (* NOTATION
  60 Notation "~ x" := (not x) : type_scope.
  61 *)
  62
  63 (* NOTATION
  64 Notation "A <-> B" := (iff A B) : type_scope.
  65 *)
  66
  67 (* NOTATION
  68 Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
  69   (at level 200) : type_scope.
  70 *)
  71
  72 (* NOTATION
  73 Notation "'exists' x , p" := (ex (fun x => p))
  74   (at level 200, x ident) : type_scope.
  75 *)
  76
  77 (* NOTATION
  78 Notation "'exists' x : t , p" := (ex (fun x:t => p))
  79   (at level 200, x ident, format "'exists'  '/  ' x  :  t ,  '/  ' p")
  80   : type_scope.
  81 *)
  82
  83 (* NOTATION
  84 Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
  85   (at level 200, x ident, p at level 200) : type_scope.
  86 *)
  87
  88 (* NOTATION
  89 Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
  90   (at level 200, x ident, t at level 200, p at level 200,
  91    format "'exists2'  '/  ' x  :  t ,  '/  ' '[' p  &  '/' q ']'")
  92   : type_scope.
  93 *)
  94
  95 (* NOTATION
  96 Notation "x = y" := (x = y :>_) : type_scope.
  97 *)
  98
  99 (* NOTATION
 100 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
 101 *)
 102
 103 (* NOTATION
 104 Notation "x <> y" := (x <> y :>_) : type_scope.
 105 *)
 106
 107 (* From Init/Notations ****************************************************)
 108
 109 (* NOTATION
 110 Reserved Notation "x <-> y" (at level 95, no associativity).
 111 *)
 112
 113 (* NOTATION
 114 Reserved Notation "x /\ y" (at level 80, right associativity).
 115 *)
 116
 117 (* NOTATION
 118 Reserved Notation "x \/ y" (at level 85, right associativity).
 119 *)
 120
 121 (* NOTATION
 122 Reserved Notation "~ x" (at level 75, right associativity).
 123 *)
 124
 125 (* NOTATION
 126 Reserved Notation "x = y  :> T"
 127 (at level 70, y at next level, no associativity).
 128 *)
 129
 130 (* NOTATION
 131 Reserved Notation "x = y" (at level 70, no associativity).
 132 *)
 133
 134 (* NOTATION
 135 Reserved Notation "x = y = z"
 136 (at level 70, no associativity, y at next level).
 137 *)
 138
 139 (* NOTATION
 140 Reserved Notation "x <> y  :> T"
 141 (at level 70, y at next level, no associativity).
 142 *)
 143
 144 (* NOTATION
 145 Reserved Notation "x <> y" (at level 70, no associativity).
 146 *)
 147
 148 (* NOTATION
 149 Reserved Notation "x <= y" (at level 70, no associativity).
 150 *)
 151
 152 (* NOTATION
 153 Reserved Notation "x < y" (at level 70, no associativity).
 154 *)
 155
 156 (* NOTATION
 157 Reserved Notation "x >= y" (at level 70, no associativity).
 158 *)
 159
 160 (* NOTATION
 161 Reserved Notation "x > y" (at level 70, no associativity).
 162 *)
 163
 164 (* NOTATION
 165 Reserved Notation "x <= y <= z" (at level 70, y at next level).
 166 *)
 167
 168 (* NOTATION
 169 Reserved Notation "x <= y < z" (at level 70, y at next level).
 170 *)
 171
 172 (* NOTATION
 173 Reserved Notation "x < y < z" (at level 70, y at next level).
 174 *)
 175
 176 (* NOTATION
 177 Reserved Notation "x < y <= z" (at level 70, y at next level).
 178 *)
 179
 180 (* NOTATION
 181 Reserved Notation "x + y" (at level 50, left associativity).
 182 *)
 183
 184 (* NOTATION
 185 Reserved Notation "x - y" (at level 50, left associativity).
 186 *)
 187
 188 (* NOTATION
 189 Reserved Notation "x * y" (at level 40, left associativity).
 190 *)
 191
 192 (* NOTATION
 193 Reserved Notation "x / y" (at level 40, left associativity).
 194 *)
 195
 196 (* NOTATION
 197 Reserved Notation "- x" (at level 35, right associativity).
 198 *)
 199
 200 (* NOTATION
 201 Reserved Notation "/ x" (at level 35, right associativity).
 202 *)
 203
 204 (* NOTATION
 205 Reserved Notation "x ^ y" (at level 30, right associativity).
 206 *)
 207
 208 (* NOTATION
 209 Reserved Notation "( x , y , .. , z )" (at level 0).
 210 *)
 211
 212 (* NOTATION
 213 Reserved Notation "{ x }" (at level 0, x at level 99).
 214 *)
 215
 216 (* NOTATION
 217 Reserved Notation "{ A } + { B }" (at level 50, left associativity).
 218 *)
 219
 220 (* NOTATION
 221 Reserved Notation "A + { B }" (at level 50, left associativity).
 222 *)
 223
 224 (* NOTATION
 225 Reserved Notation "{ x : A  |  P }" (at level 0, x at level 99).
 226 *)
 227
 228 (* NOTATION
 229 Reserved Notation "{ x : A  |  P  &  Q }" (at level 0, x at level 99).
 230 *)
 231
 232 (* NOTATION
 233 Reserved Notation "{ x : A  &  P }" (at level 0, x at level 99).
 234 *)
 235
 236 (* NOTATION
 237 Reserved Notation "{ x : A  &  P  &  Q }" (at level 0, x at level 99).
 238 *)
 239
 240 (* From Init/Peano ********************************************************)
 241
 242 (* NOTATION
 243 Infix "+" := plus : nat_scope.
 244 *)
 245
 246 (* NOTATION
 247 Infix "*" := mult : nat_scope.
 248 *)
 249
 250 (* NOTATION
 251 Infix "-" := minus : nat_scope.
 252 *)
 253
 254 (* NOTATION
 255 Infix "<=" := le : nat_scope.
 256 *)
 257
 258 (* NOTATION
 259 Infix "<" := lt : nat_scope.
 260 *)
 261
 262 (* NOTATION
 263 Infix ">=" := ge : nat_scope.
 264 *)
 265
 266 (* NOTATION
 267 Infix ">" := gt : nat_scope.
 268 *)
 269
 270 (* NOTATION
 271 Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
 272 *)
 273
 274 (* NOTATION
 275 Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
 276 *)
 277
 278 (* NOTATION
 279 Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
 280 *)
 281
 282 (* NOTATION
 283 Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
 284 *)
 285
 286 (* From Init/Specif *******************************************************)
 287
 288 (* NOTATION
 289 Notation "{ x : A  |  P }" := (sig (fun x:A => P)) : type_scope.
 290 *)
 291
 292 (* NOTATION
 293 Notation "{ x : A  |  P  &  Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
 294   type_scope.
 295 *)
 296
 297 (* NOTATION
 298 Notation "{ x : A  &  P }" := (sigS (fun x:A => P)) : type_scope.
 299 *)
 300
 301 (* NOTATION
 302 Notation "{ x : A  &  P  &  Q }" := (sigS2 (fun x:A => P) (fun x:A => Q)) :
 303   type_scope.
 304 *)
 305
 306 (* NOTATION
 307 Add Printing Let sig.
 308 *)
 309
 310 (* NOTATION
 311 Add Printing Let sig2.
 312 *)
 313
 314 (* NOTATION
 315 Add Printing Let sigS.
 316 *)
 317
 318 (* NOTATION
 319 Add Printing Let sigS2.
 320 *)
 321
 322 (* NOTATION
 323 Add Printing If sumbool.
 324 *)
 325
 326 (* NOTATION
 327 Add Printing If sumor.
 328 *)
 329
 330 (* From Lists/List ********************************************************)
 331
 332 (* NOTATION
 333 Infix "::" := cons (at level 60, right associativity) : list_scope.
 334 *)
 335
 336 (* NOTATION
 337 Infix "++" := app (right associativity, at level 60) : list_scope.
 338 *)
 339
 340 (* NOTATION
 341 Infix "::" := cons (at level 60, right associativity) : list_scope.
 342 *)
 343
 344 (* NOTATION
 345 Infix "++" := app (right associativity, at level 60) : list_scope.
 346 *)
 347
 348 (* From Num/Leibniz/EqAxioms **********************************************)
 349
 350 (* NOTATION
 351 Grammar constr constr1 :=
 352 eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
 353 *)
 354
 355 (* NOTATION
 356 Syntax constr
 357   level 1:
 358     equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ].
 359 *)
 360
 361 (* From Num/Leibniz/NSyntax ***********************************************)
 362
 363 (* NOTATION
 364 Infix 6 "<" lt.
 365 *)
 366
 367 (* NOTATION
 368 Infix 6 "<=" le.
 369 *)
 370
 371 (* NOTATION
 372 Infix 6 ">" gt.
 373 *)
 374
 375 (* NOTATION
 376 Infix 6 ">=" ge.
 377 *)
 378
 379 (* NOTATION
 380 Grammar constr lassoc_constr4 :=
 381   squash_sum
 382   [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
 383       case [$c2] of
 384         (SQUASH $T2) ->
 385             case [$c1] of
 386               (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
 387             | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
 388             esac
 389       | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
 390       esac.
 391 *)
 392
 393 (* NOTATION
 394 Syntax constr
 395   level 1:
 396     equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
 397  ;
 398
 399   level 4:
 400     sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
 401 .
 402 *)
 403
 404 (* From Num/Nat/NSyntax ***************************************************)
 405
 406 (* NOTATION
 407 Infix 6 "<" lt.
 408 *)
 409
 410 (* NOTATION
 411 Infix 6 "<=" le.
 412 *)
 413
 414 (* NOTATION
 415 Infix 6 ">" gt.
 416 *)
 417
 418 (* NOTATION
 419 Infix 6 ">=" ge.
 420 *)
 421
 422 (* NOTATION
 423 Grammar constr lassoc_constr4 :=
 424   squash_sum
 425   [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
 426       case [$c2] of
 427         (SQUASH $T2) ->
 428             case [$c1] of
 429               (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
 430             | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
 431             esac
 432       | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
 433       esac.
 434 *)
 435
 436 (* NOTATION
 437 Syntax constr
 438   level 4:
 439     sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
 440 .
 441 *)
 442
 443 (* From Num/EqParams ******************************************************)
 444
 445 (* NOTATION
 446 Grammar constr constr1 :=
 447 eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ].
 448 *)
 449
 450 (* NOTATION
 451 Syntax constr
 452   level 1:
 453     equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1]  "=" $t2:E ] ]
 454 .
 455 *)
 456
 457 (* From Num/NSyntax *******************************************************)
 458
 459 (* NOTATION
 460 Infix 6 "<" lt V8only 70.
 461 *)
 462
 463 (* NOTATION
 464 Infix 6 "<=" le V8only 70.
 465 *)
 466
 467 (* NOTATION
 468 Infix 6 ">" gt V8only 70.
 469 *)
 470
 471 (* NOTATION
 472 Infix 6 ">=" ge V8only 70.
 473 *)
 474
 475 (* NOTATION
 476 Grammar constr lassoc_constr4 :=
 477   squash_sum
 478   [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
 479       case [$c2] of
 480         (SQUASH $T2) ->
 481             case [$c1] of
 482               (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
 483             | $_           -> [ (sumor $c1 $T2) ]   (* c1+{T2} *)
 484             esac
 485       | $_           -> [ (add $c1 $c2) ]           (* c1+c2 *)
 486       esac.
 487 *)
 488
 489 (* NOTATION
 490 Syntax constr
 491   level 4:
 492     sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
 493 .
 494 *)
 495
 496 (* From Num/NeqDef ********************************************************)
 497
 498 (* NOTATION
 499 Infix 6 "<>" neq V8only 70.
 500 *)
 501
 502 (* From Num/NeqParams *****************************************************)
 503
 504 (* NOTATION
 505 Infix 6 "<>" neq V8only 70.
 506 *)
 507
 508 (* From Reals/RIneq *******************************************************)
 509
 510 (* NOTATION
 511 Add Field R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RTheory Rinv_l
 512  with minus := Rminus div := Rdiv.
 513 *)
 514
 515 (* From Reals/Ranalysis1 **************************************************)
 516
 517 (* NOTATION
 518 Infix "+" := plus_fct : Rfun_scope.
 519 *)
 520
 521 (* NOTATION
 522 Notation "- x" := (opp_fct x) : Rfun_scope.
 523 *)
 524
 525 (* NOTATION
 526 Infix "*" := mult_fct : Rfun_scope.
 527 *)
 528
 529 (* NOTATION
 530 Infix "-" := minus_fct : Rfun_scope.
 531 *)
 532
 533 (* NOTATION
 534 Infix "/" := div_fct : Rfun_scope.
 535 *)
 536
 537 (* NOTATION
 538 Notation Local "f1 'o' f2" := (comp f1 f2)
 539   (at level 20, right associativity) : Rfun_scope.
 540 *)
 541
 542 (* NOTATION
 543 Notation "/ x" := (inv_fct x) : Rfun_scope.
 544 *)
 545
 546 (* From Reals/Rdefinitions ************************************************)
 547
 548 (* NOTATION
 549 Infix "+" := Rplus : R_scope.
 550 *)
 551
 552 (* NOTATION
 553 Infix "*" := Rmult : R_scope.
 554 *)
 555
 556 (* NOTATION
 557 Notation "- x" := (Ropp x) : R_scope.
 558 *)
 559
 560 (* NOTATION
 561 Notation "/ x" := (Rinv x) : R_scope.
 562 *)
 563
 564 (* NOTATION
 565 Infix "<" := Rlt : R_scope.
 566 *)
 567
 568 (* NOTATION
 569 Infix "-" := Rminus : R_scope.
 570 *)
 571
 572 (* NOTATION
 573 Infix "/" := Rdiv : R_scope.
 574 *)
 575
 576 (* NOTATION
 577 Infix "<=" := Rle : R_scope.
 578 *)
 579
 580 (* NOTATION
 581 Infix ">=" := Rge : R_scope.
 582 *)
 583
 584 (* NOTATION
 585 Infix ">" := Rgt : R_scope.
 586 *)
 587
 588 (* NOTATION
 589 Notation "x <= y <= z" := ((x <= y)%R /\ (y <= z)%R) : R_scope.
 590 *)
 591
 592 (* NOTATION
 593 Notation "x <= y < z" := ((x <= y)%R /\ (y < z)%R) : R_scope.
 594 *)
 595
 596 (* NOTATION
 597 Notation "x < y < z" := ((x < y)%R /\ (y < z)%R) : R_scope.
 598 *)
 599
 600 (* NOTATION
 601 Notation "x < y <= z" := ((x < y)%R /\ (y <= z)%R) : R_scope.
 602 *)
 603
 604 (* From Reals/Rfunctions **************************************************)
 605
 606 (* NOTATION
 607 Infix "^" := pow : R_scope.
 608 *)
 609
 610 (* NOTATION
 611 Infix Local "^Z" := powerRZ (at level 30, right associativity) : R_scope.
 612 *)
 613
 614 (* From Reals/Rpower ******************************************************)
 615
 616 (* NOTATION
 617 Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope.
 618 *)
 619
 620 (* From Reals/Rtopology ***************************************************)
 621
 622 (* NOTATION
 623 Infix "=_D" := eq_Dom (at level 70, no associativity).
 624 *)
 625
 626 (* From Setoids/Setoid ****************************************************)
 627
 628 (* NOTATION
 629 Add Setoid Prop iff Prop_S.
 630 *)
 631
 632 (* From Wellfounded/Disjoint_Union ****************************************)
 633
 634 (* NOTATION
 635 Notation Le_AsB := (le_AsB A B leA leB).
 636 *)
 637
 638 (* From Wellfounded/Lexicographic_Product *********************************)
 639
 640 (* NOTATION
 641 Notation LexProd := (lexprod A B leA leB).
 642 *)
 643
 644 (* NOTATION
 645 Notation Symprod := (symprod A B leA leB).
 646 *)
 647
 648 (* NOTATION
 649 Notation SwapProd := (swapprod A R).
 650 *)
 651
 652 (* From Wellfounded/Union *************************************************)
 653
 654 (* NOTATION
 655 Notation Union := (union A R1 R2).
 656 *)
 657
 658 (* From Wellfounded/Lexicographic_Exponentiation **************************)
 659
 660 (* NOTATION
 661 Notation Power := (Pow A leA).
 662 *)
 663
 664 (* NOTATION
 665 Notation Lex_Exp := (lex_exp A leA).
 666 *)
 667
 668 (* NOTATION
 669 Notation ltl := (Ltl A leA).
 670 *)
 671
 672 (* NOTATION
 673 Notation Descl := (Desc A leA).
 674 *)
 675
 676 (* NOTATION
 677 Notation List := (list A).
 678 *)
 679
 680 (* NOTATION
 681 Notation Nil := (nil (A:=A)).
 682 *)
 683
 684 (* NOTATION
 685 Notation Cons := (cons (A:=A)).
 686 *)
 687
 688 (* NOTATION
 689 Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).
 690 *)
 691
 692 (* From Wellfounded/Transitive_Closure ************************************)
 693
 694 (* NOTATION
 695 Notation trans_clos := (clos_trans A R).
 696 *)
 697
 698 (* From ZArith/Zdiv *******************************************************)
 699
 700 (* NOTATION
 701 Infix "/" := Zdiv : Z_scope.
 702 *)
 703
 704 (* NOTATION
 705 Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
 706 *)
 707
 708 (* From ZArith/Zpower *****************************************************)
 709
 710 (* NOTATION
 711 Infix "^" := Zpower : Z_scope.
 712 *)
 713
 714 (* NOTATION
 715 Infix "^" := Zpower : Z_scope.
 716 *)
 717
 718 (* From ZArith/BinInt *****************************************************)
 719
 720 (* NOTATION
 721 Infix "+" := Zplus : Z_scope.
 722 *)
 723
 724 (* NOTATION
 725 Notation "- x" := (Zopp x) : Z_scope.
 726 *)
 727
 728 (* NOTATION
 729 Infix "-" := Zminus : Z_scope.
 730 *)
 731
 732 (* NOTATION
 733 Infix "*" := Zmult : Z_scope.
 734 *)
 735
 736 (* NOTATION
 737 Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.
 738 *)
 739
 740 (* NOTATION
 741 Infix "<=" := Zle : Z_scope.
 742 *)
 743
 744 (* NOTATION
 745 Infix "<" := Zlt : Z_scope.
 746 *)
 747
 748 (* NOTATION
 749 Infix ">=" := Zge : Z_scope.
 750 *)
 751
 752 (* NOTATION
 753 Infix ">" := Zgt : Z_scope.
 754 *)
 755
 756 (* NOTATION
 757 Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
 758 *)
 759
 760 (* NOTATION
 761 Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
 762 *)
 763
 764 (* NOTATION
 765 Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
 766 *)
 767
 768 (* NOTATION
 769 Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
 770 *)
 771
 772 (* From ZArith/Znumtheory *************************************************)
 773
 774 (* NOTATION
 775 Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
 776 *)
 777
 778 (* From NArith/BinNat *****************************************************)
 779
 780 (* NOTATION
 781 Infix "+" := Nplus : N_scope.
 782 *)
 783
 784 (* NOTATION
 785 Infix "*" := Nmult : N_scope.
 786 *)
 787
 788 (* NOTATION
 789 Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
 790 *)
 791
 792 (* From NArith/BinPos *****************************************************)
 793
 794 (* NOTATION
 795 Infix "+" := Pplus : positive_scope.
 796 *)
 797
 798 (* NOTATION
 799 Infix "-" := Pminus : positive_scope.
 800 *)
 801
 802 (* NOTATION
 803 Infix "*" := Pmult : positive_scope.
 804 *)
 805
 806 (* NOTATION
 807 Infix "/" := Pdiv2 : positive_scope.
 808 *)
 809
 810 (* NOTATION
 811 Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
 812 *)
 813