
#ifndef IOTALOGIC_H_INCLUDED
#define IOTALOGIC_H_INCLUDED

#include "typedefs.h"

/*@
  predicate
   Iota(value_type* a, integer n, value_type v) = 
     \forall integer i; 0 <= i < n ==> a[i] == v+i; 
*/

#endif /* IOTALOGIC_H_INCLUDED */

