Some definitions of interest. | |
array | Def array(T) == n:![]() ![]() ![]() ![]() ![]() |
Thm* ![]() ![]() | |
array-update | Def a[i:=v] == < |a|,![]() ![]() ![]() |
array-length | Def |a| == 1of(a) |
array-select | Def a[i] == 2of(a)(i) |
sum | Def sum(f(x) | x < k) == primrec(k;0;![]() |
Thm* ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
eq_int | Def i=![]() ![]() ![]() ![]() |
Thm* ![]() ![]() ![]() ![]() ![]() | |
int_seg | Def {i..j![]() ![]() ![]() |
Thm* ![]() ![]() ![]() ![]() | |
nat | Def ![]() ![]() ![]() |
Thm* ![]() ![]() |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() |