[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 list-as-arrayinstance
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