title: Modelling generic datatypes for Z3 and or SMT(v2.6)
body: <p>I would like to model the behaviour of generic datatypes in SMT v2.6. I am using Z3 as constraint solver. I modelled, based on the <a href="https://rise4fun.com/Z3/775?frame=1&amp;menu=0&amp;course=1" rel="nofollow noreferrer">official example</a>, a generic list as parameterised datatype in the following way:</p>
  
  <pre><code>(declare-datatypes (T) ((MyList nelem (cons (hd T) (tl MyList)))))
  </code></pre>
  
  <p>I would like the list to be generic with respect to the datatype. Later on, I would like to declare constants the following way:</p>
  
  <pre><code>(declare-const x (MyList Int))
  (declare-const y (MyList Real))
  </code></pre>
  
  <p>However, now I would like to define functions on the generic datatype <code>MyList</code> (e.g., a length operation, empty operation, ...) so that they are re-usable for all <code>T</code>'s. Do you have an idea how I could achieve this? I did try something like:</p>
  
  <pre><code>(declare-sort K)
  (define-fun isEmpty ((in (MyList K))) Bool
      (= in nelem)
  ) 
  </code></pre>
  
  <p>but this gives me an error message; for this example to work Z3 would need to do some type-inference, I suppose.</p>
  
  <p>Would be great if you could could give me a hint. </p>