matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl

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