matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl

   1 name "ground_2_src"
   2
   3 table {
   4    class "gray"
   5    [ { "component" * } {
   6         [ { "plane" * } {
   7              [ "files" * ]
   8           }
   9         ]
  10      }
  11    ]
  12    class "water"
  13    [ { "generic rt-transition counter" * } {
  14         [ { "" * } {
  15              [ "rtc_ist ( 𝐓❪?,?❫ )" "rtc_ist_shift" "rtc_ist_plus" "rtc_ist_max" * ]
  16              [ "rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )" "rtc_isrc ( 𝐑𝐓❪?,?❫ )" "rtc_shift ( ↕*? )" "rtc_max ( ? ∨ ? )" "rtc_plus ( ? + ? )" * ]
  17           }
  18         ]
  19      }
  20    ]
  21    class "green"
  22    [ { "multiple relocation" * } {
  23         [ { "" * } {
  24              [ "rtmap" "rtmap_eq ( ? ≡ ? )" "rtmap_pushs ( ⫯*[?]? )" "rtmap_nexts ( ↑*[?]? )"
  25                "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈❪?❫ )" "rtmap_id" "rtmap_isdiv ( 𝛀❪?❫ )"
  26                "rtmap_fcla ( 𝐂❪?❫ ≘ ? )" "rtmap_isfin ( 𝐅❪?❫ )" "rtmap_isuni ( 𝐔❪?❫ )" "rtmap_uni ( 𝐔❨?❩ )"
  27                "rtmap_sle ( ? ⊆ ? )" "rtmap_sdj ( ? ∥ ? )" "rtmap_sand ( ? ⋒ ? ≘ ? )" "rtmap_sor ( ? ⋓ ? ≘ ? )"
  28                "rtmap_at ( @❪?,?❫ ≘ ? )" "rtmap_istot ( 𝐓❪?❫ )" "rtmap_after ( ? ⊚ ? ≘ ? )" "rtmap_coafter ( ? ~⊚ ? ≘ ? )"
  29                "rtmap_basic ( 𝐁❨?,?❩ )" "rtmap_basic_after"
  30              * ]
  31              [ "nstream ( ⫯? ) ( ↑? )" "nstream_eq" "" ""
  32                "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" ""
  33                "" "" "" ""
  34                "" "" "" "nstream_sor"
  35                "" "nstream_istot ( ?@❨?❩ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
  36                "nstream_basic" ""
  37              * ]
  38 (*
  39              [ "trace ( ∥?∥ )" "trace_at ( @❪?,?❫ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈❪?❫ )" "trace_isun ( 𝐔❪?❫ )"
  40                "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≘ ? )" "trace_snot ( ∁ ? )" * ]
  41 *)
  42              [ "mr2 ( ◊ ) ( ❨?,?❩;? )" "mr2_at ( @❪?,?❫ ≘ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≘ ? )" * ]
  43           }
  44         ]
  45      }
  46    ]
  47    class "grass"
  48    [ { "natural numbers with infinity" * } {
  49         [ { "" * } {
  50            [ "ynat ( ∞ )" "ynat_pred ( ↓? )" "ynat_succ ( ↑? )"
  51              "ynat_le ( ? ≤ ? )" "ynat_lt ( ? &lt; ? )"
  52              "ynat_plus ( ? + ? )" *
  53            ]
  54           }
  55         ]
  56      }
  57    ]
  58    class "yellow"
  59    [ { "extensions to the library" * } {
  60         [ { "" * } {
  61              [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
  62              [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ]
  63              [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" "arith_2a" "arith_2b" * ]
  64              [ "ltc" "ltc_ctc" * ]
  65              [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" * ]
  66           }
  67         ]
  68      }
  69    ]
  70    class "orange"
  71    [ { "generated library" * } {
  72         [ { "generalization with equality" * } {
  73              [ "insert_eq" * ]
  74           }
  75         ]
  76         [ { "permutation of quantifiers" * } {
  77              [ "pull" * ]
  78           }
  79         ]
  80         [ { "logical decomposables" * } {
  81              [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" * ]
  82           }
  83         ]
  84      }
  85    ]
  86    class "red"
  87    [ { "" * } {
  88         [ { "" * } {
  89              [ * ]
  90           }
  91         ]
  92      }
  93    ]
  94 }
  95
  96 class "top"               { * }
  97
  98 class "capitalize italic" { 0 }
  99
 100 class "italic"            { 1 }