Email Gateway (Aug 18 2022 at 09:45): Email Gateway (Aug 18 2022 at 09:45):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Hello,
I have created an I/O automaton using the Isabelle syntax in HOLCF/IOA.
Now I have a problem.
Can I create an automaton in a function?
What I want is something like this:
defs
fdef:
"f a == automaton auto =
signature
actions "enne action"
...."
but the problem is that the definition of the function require a string,
but when I insert the function body between two " Isabelle give me a syntax
error.
I tried to use the escape sequence for " that is \" but Isabelle return a
lexical error in the definition of the states.
There is another way to do that?
Thanks
Gabriele
Email Gateway (Aug 18 2022 at 09:45):From: Tobias Nipkow <nipkow@in.tum.de>
You cannot mix the two levels, i.e. you cannot embed theory commands
inside a formula.
Tobias
Gabriele Pozzani wrote:
Last updated: May 03 2024 at 04:19 UTC