category | objects |
|
|
|
|
|
sizes | files | 102 | characters | 143239 | nodes | 332314 |
propositions | theorems | 42 | lemmas | 679 | total | 721 |
concepts | declared | 65 | defined | 70 | total | 135 |
component | plane | files |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
generic rt-transition counter | rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 ) | rtc_isrc ( 𝐑𝐓⦃?, ?⦄ ) | rtc_shift ( ↓? ) | rtc_max ( ? ∨ ? ) | rtc_plus ( ? + ? ) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
multiple relocation | rtmap | rtmap_eq ( ? ≗ ? ) | rtmap_pushs ( ↑*[?]? ) | rtmap_nexts ( ⫯*[?]? ) | rtmap_tl ( ⫱? ) | rtmap_tls ( ⫱*[?]? ) | rtmap_isid ( 𝐈⦃?⦄ ) | rtmap_id | rtmap_isdiv ( 𝛀⦃?⦄ ) | rtmap_fcla ( 𝐂⦃?⦄ ≡ ? ) | rtmap_isfin ( 𝐅⦃?⦄ ) | rtmap_isuni ( 𝐔⦃?⦄ ) | rtmap_uni ( 𝐔❴?❵ ) | rtmap_sle ( ? ⊆ ? ) | rtmap_sand ( ? ⋒ ? ≡ ? ) | rtmap_sor ( ? ⋓ ? ≡ ? ) | rtmap_at ( @⦃?,?⦄ ≡ ? ) | rtmap_istot ( 𝐓⦃?⦄ ) | rtmap_after ( ? ⊚ ? ≡ ? ) | rtmap_coafter ( ? ~⊚ ? ≡ ? ) | |
|
|
nstream ( ↑? ) ( ⫯? ) | nstream_eq | nstream_isid | nstream_id ( 𝐈𝐝 ) | nstream_sor | nstream_istot ( ?@❴?❵ ) | nstream_after ( ? ∘ ? ) | nstream_coafter ( ? ~∘ ? ) | ||||||||||||
|
|
mr2 | mr2_at ( @⦃?,?⦄ ≡ ? ) | mr2_plus ( ? + ? ) | mr2_minus ( ? ▭ ? ≡ ? ) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
natural numbers with infinity | ynat ( ∞ ) | ynat_pred ( ⫰? ) | ynat_succ ( ⫯? ) | ynat_le ( ? ≤ ? ) | ynat_lt ( ? < ? ) | ynat_plus ( ? + ? ) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
extensions to the library | stream ( ? @ ? ) | stream_eq ( ? ≐ ? ) | stream_hdtl ( ↓? ) | stream_tls ( ↓*[?]? ) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
list ( ◊ ) ( ? @ ? ) ( |?| ) | list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
bool ( Ⓕ ) ( Ⓣ ) | arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? ) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
relations | star | lstar |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
generated logical decomposables | xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ ) | xoa_props ( ⊥ ) ( ⊤ ) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|