Re: [isabelle] Separating function declaration from implementation

> You are right. This is why primrec will also change its syntax to the
> simultaneous style. The new syntax, which works just like "function", is
> already supported (and preferred) in the developers version.
> Eventually, primitive "const" declarations will mostly disappear from
> user theories, and you will use the "definition", "inductive",
> "primrec", "function"... packages, which all share a common syntax.

It is worth noting that future Isabelle versions still technically will
permit to separate constant declaration from constant definition by
means of the overloading target:

consts foo :: "'a => 'a"

  foo == "foo :: 'a => 'a"

definition foo :: "'a => 'a" where
  "foo x = x"


thm foo_def

Obviously, this only works on the theory level (not in locales etc.).
Presumably this was one reason to sacrifice the separation of consts and
 defs on the Isar level.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.