Specification get-outside

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

enrich
   array
with
   comment: restricts array-get to be compatible with the definition of get on lists;
   variables 
       ar : array;
       n : nat;
   
   
   axioms 
      get-outside: # ar ≤ n → ar[n] = mkarray(0)[n - # ar];
      comment: this constraint is implied by the recursive definition of list-get, but not for array-get;
   
   
end enrich