doc-src/Tutorial/Recdef/sep1
author skalberg
Thu, 09 Oct 2003 18:13:32 +0200
changeset 14223 0ee05eef881b
parent 6100 40d66bc3e83f
permissions -rw-r--r--
Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).

recdef sep "measure (%(a,xs). length xs)"
  "sep(a, x#y#zs) = x # a # sep(a,y#zs)"
  "sep(a, xs)     = xs"