Email Gateway (Aug 18 2022 at 18:25): Email Gateway (Aug 18 2022 at 18:25):From: Steve Wong <s.wong.731@gmail.com>
Hi,
I have two questions regarding implementing ML functions:
1) If I have a file containing my own ML function "foo" in a structure
"bar", I seem to have to call "bar" using "foo.bar". I see that the
functions in BasicLibrary, Term, etc., one could call "maps" by just "maps"
and not "BasicLibrary.maps". So how should "bar" be defined in order to be
able to call "foo" with just "foo"?
2) If my functions spread over numerous files, is there a neat way for
including all these files in a .thy rather than 10 or so individual lines of
'use "..."'?
Thanks!
Steve
Email Gateway (Aug 18 2022 at 18:25):From: Makarius <makarius@sketis.net>
On Fri, 23 Sep 2011, Steve Wong wrote:
I have two questions regarding implementing ML functions:
1) If I have a file containing my own ML function "foo" in a structure
"bar", I seem to have to call "bar" using "foo.bar". I see that the
functions in BasicLibrary, Term, etc., one could call "maps" by just "maps"
and not "BasicLibrary.maps". So how should "bar" be defined in order to be
able to call "foo" with just "foo"?
The idea is to wrap things in structures by default, and only make parts
of the content pervasive later, either by 'open' of a substructure or by
individual 'val' declarations after the structure definition. Here are
some representative examples for both ways:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011/src/Pure/goal.ML
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011/src/Pure/subgoal.ML
See the start and end of these files, respectively.
2) If my functions spread over numerous files, is there a neat way for
including all these files in a .thy rather than 10 or so individual
lines of 'use "..."'?
10 'use' commands are not so much -- we do this routinely with many more
files.
You can also embed ML text directly in the theory body, using the 'ML'
command, or variations of it.
Makarius
Last updated: Apr 26 2024 at 08:19 UTC