[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('a); 
      [] → []; 
      + → +; 
      # → #; 
      < → <; 
      .head → .first; 
      .tail → .rest; 
      [ ] → ]; 
      [ ] → ]; 
   rename 
      ' → '; 
      + → +; 
      + → +; 
      +2 → +2; 
      map → map; 
      .foldLeft → .foldLeft; 
      ++ → ++; 
      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