these-jcb/code/mappingPeanoNatList.tex

\begin{tomcode}[label=code:mappingPeanoNatList,caption=Ancrage algébrique pour une liste d'entiers de Peano]
  %typeterm NatList {
    implement     { JNatList }
    is_sort(s)    { (s instanceof JNatList) }
    equals(t1,t2) { (t1.equals(t2)) }
  }

  %oplist NatList concNat(Nat*) {
    is_fsym(s)         { (s instanceof JconcJNat) }
    get_head(l)        { ((JconcJNat)l).head }
    get_tail(l)        { ((JconcJNat)l).tail }
    is_empty(l)        { ((JconcJNat)l).isEmpty() }
    make_empty()       { new JconcJNat() }
    make_insert(t,l)   { new JconcJNat(t,l) }
  }
\end{tomcode}