[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
< 
   list-perm
with 
   array-listops, 
   get-outside
   
by mapping
      : List → Array; 
      [] → []; 
       . + .  : (Elem × List → List) →  . + .  : (Elem × Array → Array); 
      # .  → # . ; 
       . < .  : (List × List → Bool) →  . < .  : (Array × Array → Bool); 
       . head →  . first; 
       . tail →  . rest; 
       . ( . )  →  . ( . ) ; 
       . (. := .)  →  . (. := .) ; 
   rename 
       . ' →  . '; 
       . + .  : (List × List → List) →  . + .  : (Array × Array → Array); 
       . + .  : (List × Elem → List) →  . + .  : (Array × Elem → Array); 
       . +2 .  →  . +2 . ; 
       . ++ .  →  . ++ . ; 
      rmdup → rmdup; 
      rev → rev; 
      mklist → mklist; 
      fillfirst → fillfirst; 
       . -l .  →  . -l . ; 
       . -1l .  →  . -1l . ; 
       . -p .  →  . -p . ; 
      pos → pos; 
      frome → frome; 
       . ∪ .  →  . ∪ . ; 
       . \ .  →  . \ . ; 
      filter → filter; 
      #oc → #oc; 
       . ∈ .  →  . ∈ . ; 
      dups → dups; 
      disj → disj; 
       . ⊑ .  →  . ⊑ . ; 
       . ⊒ .  →  . ⊒ . ; 
       . ⊆ .  →  . ⊆ . ; 
      perm → perm; 
       . ⊆m .  →  . ⊆m . ; 
       . last →  . last; 
       . butlast →  . butlast; 
      butlastn → butlastn; 
      firstn → firstn; 
      restn → restn; 
      lastn → lastn; 
      sublist → sublist; 
end instantiate