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