]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
lift functions and identity map
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / web / ground_2_src.tbl
index ae1acddff5b7308142cd46a762425a75098612b1..50896c56c0db2f22e7d4a609f078b4482142fce6 100644 (file)
@@ -12,7 +12,7 @@ table {
    class "green"
    [ { "multiple relocation" * } {
         [ { "" * } {
-             [ "nstream" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" * ]
+             [ "nstream" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" "nstream_id ( 𝐈𝐝 ) ( 𝐈⦃?⦄ )" * ]
              [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
                "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]
              [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]