Re: [isabelle] Create automaton in a function
You cannot mix the two levels, i.e. you cannot embed theory commands
inside a formula.
Gabriele Pozzani wrote:
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:
"f a == automaton auto =
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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and