| | Some definitions of interest. |
|
| array | Def array(T) == n:  n  T |
| | | Thm*  T:Type. array(T)  Type |
|
| array-count | Def array-count(v.P(v);a) == sum(if P(a[i]) 1 else 0 fi | i < |a|) |
|
| array-update | Def a[i:=v] == < |a|, j.if j= i v else a[j] fi > |
|
| array-length | Def |a| == 1of(a) |
|
| array-select | Def a[i] == 2of(a)(i) |
|
| sum | Def sum(f(x) | x < k) == primrec(k;0;x,n. n+f(x)) |
| | | Thm* n:, f:(n ). sum(f(x) | x < n) |
|
| eq_int | Def i=j == if i=j true ; false fi |
| | | Thm* i,j:. (i=j)  |
|
| int_seg | Def {i..j } == {k:| i  k < j } |
| | | Thm* m,n:. {m..n} Type |
|
| nat | Def == {i:| 0i } |
| | | Thm* Type |
