category | objects |
|
|
|
|
|
sizes | files | 95 | characters | 135595 | nodes | 314345 |
propositions | theorems | 38 | lemmas | 647 | total | 685 |
concepts | declared | 63 | defined | 67 | total | 130 |
component | plane | files |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
generic rt-transition counter | rtc ( โฉ?,?,?,?โช ) ( ๐๐ ) ( ๐๐ ) ( ๐๐ ) | rtc_isrc ( ๐๐โฆ?, ?โฆ ) | rtc_shift ( โ? ) | rtc_max ( ? โจ ? ) | rtc_plus ( ? + ? ) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
multiple relocation | rtmap | rtmap_eq ( ? โ ? ) | rtmap_pushs ( โ*[?]? ) | rtmap_tl ( โซฑ? ) | rtmap_tls ( โซฑ*[?]? ) | rtmap_isid ( ๐โฆ?โฆ ) | rtmap_id | 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_sand | 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 ( ?^? ) ( โซฏ? ) ( โซฐ? ) ( ? โจ ? ) ( ? โง ? ) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
star | lstar |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
generated logical decomposables | xoa ( โโ ) ( โจโจ ) ( โงโง ) | xoa_props ( โฅ ) ( โค ) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|