[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,

Specification woarray
instantiate parameter
   filter-count
< 
   wolist
with 
   list-as-arrayinstance, 
   gen-weakord
   
by mapping
      : List[A] → Array[A]; 
      [] → [] : Array[A]; 
       . ' → mkar' : (A → Array[A]); 
       . +2 .  →  . +2a .  : (A × A → Array[A]); 
      mklist → mkinitar : (A × Nat → Array[A]); 
       . + .  : (A × List[A] → List[A]) →  . + .  : (A × Array[A] → Array[A]); 
      # .  → # .  : (Array[A] → Nat); 
       . + .  : (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)]); 
       . < .  : (List[A] × List[A] → Bool) →  . < .  : (Array[A] × Array[A] → Bool); 
       . ∈ .  →  . ∈ .  : (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); 
       . head →  . first : (Array[A] → A); 
       . tail →  . rest : (Array[A] → Array[A]); 
       . ( . )  →  . ( . ) : (Array[A] × Nat → A) ; 
       . (. := .)  →  . (. := .) : (Array[A] × Nat × A → Array[A]) ; 
       . 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; 
   rename 
      ins≤ → ins≤; 
      merge → merge; 
      ordered≤ → ordered≤; 
      ordered< → ordered<; 
end instantiate