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"

overloading
  foo == "foo :: 'a => 'a"
begin

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

end

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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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