[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
instantiate parameter
list-getput
<
filter-count
with
array-listops,
get-outside
by mapping
: List[A] → Array[A];
[] → [] : Array[A];
. + . : (A × List[A] → List[A]) → . + . : (A × Array[A] → Array[A]);
# . → # . : (Array[A] → Nat);
. < . : (List[A] × List[A] → Bool) → . < . : (Array[A] × Array[A] → Bool);
. head → . first : (Array[A] → A);
. tail → . rest : (Array[A] → Array[A]);
. ( . ) → . ( . ) : (Array[A] × Nat → A) ;
. (. := .) → . (. := .) : (Array[A] × Nat × A → Array[A]) ;
rename
' → mkar' prio 0;
+2 → . +2a . ;
mklist → mkinitar;
. + . : (List[A] × List[A] → List[A]) → . + . : (Array[A] × Array[A] → Array[A]);
. + . : (List[A] × A → List[A]) → . + . : (Array[A] × A → Array[A]);
. map( . ) + opttype → . map( . ) + opttype;
. foldLeft( . ) + opttype → . foldLeft( . ) + opttype;
. ++ . → . ++ . : (Array[A] × A → Array[A]);
. distinct → . distinct : (Array[A] → Array[A]);
rev → rev : (Array[A] → Array[A]);
fillfirst → fillfirst : (Nat × A × Array[A] → Array[A]);
. -l . → . -l . : (Array[A] × A → Array[A]);
. -1l . → . -1l . : (Array[A] × A → Array[A]);
. -p . → . -p . : (Array[A] × Nat → Array[A]);
. indexOf( . ) + opttype → . indexOf( . ) + opttype;
frome → frome : (Array[A] × A → Array[A]);
. ∪ . → . ∪ . : (Array[A] × Array[A] → Array[A]);
. \ . → . \ . : (Array[A] × Array[A] → Array[A]);
. intersect . → . intersect . : (Array[A] × Array[A] → Array[A]);
#oc → #oc : (A × Array[A] → Nat);
. count( . ) + opttype → . count( . ) + opttype;
. filter( . ) + opttype → . filter( . ) + opttype;
. zip . → . zip . : (Array[A] × Array[B] → Array[(A × B)]);
. ∈ . → . ∈ . : (A × Array[A] → Bool);
dups → dups : (Array[A] → Bool);
disj → disj : (Array[A] × Array[A] → Bool);
. ⊑ . → . ⊑ . : (Array[A] × Array[A] → Bool);
. ⊒ . → . ⊒ . : (Array[A] × Array[A] → Bool);
. ⊆ . → . ⊆ . : (Array[A] × Array[A] → Bool);
perm → perm : (Array[A] × Array[A] → Bool);
. ⊆m . → . ⊆m . : (Array[A] × Array[A] → Bool);
. last → . last : (Array[A] → A);
. butlast → . butlast : (Array[A] → Array[A]);
. dropRight( . ) + opttype → . dropRight( . ) + opttype;
. take( . ) + opttype → . take( . ) + opttype;
. drop( . ) + opttype → . drop( . ) + opttype;
. takeRight( . ) + opttype → . takeRight( . ) + opttype;
. sublist( . ) + opttype → . sublist( . ) + opttype;
. count( . ) + opttype → . count( . ) + opttype;
end instantiate