Email Gateway (Aug 18 2022 at 11:15): Email Gateway (Aug 18 2022 at 11:15):From: George Karabotsos <g_karab@cs.concordia.ca>
Hello,
I have seen numerous definition statements in the HOL.*.thy theories.
They seem to just be synonymous to fun/function declarations. Is
definition a synonym of fun/function or there are more differences?
TIA,
George
Email Gateway (Aug 18 2022 at 11:15):From: Alexander Krauss <krauss@in.tum.de>
Hi George,
"definition" does just basic definitions of the form
"f x y z = rhs x y z"
In particular, it does not allow recursion or pattern matching. "fun"
and "function" do that, and call "definition" (at least something like
it) internally.
Another difference is that definition is a general concept from
Isabelle/Pure, whereas fun only exists in HOL.
In HOL, one could actually use fun wherever definition is used (except
for the early HOL theories where it is not yet available), but it is
often a bit of an overkill.
Alex
Last updated: May 03 2024 at 12:27 UTC