Thomas Sewell writes:
>
> BTW, should I have known this already? Is there some part of the
> documentation that I should have read, but have overlooked?
Sort of. Both functions are used in an example in the Programming
Tutorial[*] on page 19. What the function check_term does is a bit
more
On Tue, 9 Feb 2010, Thomas Sewell wrote:
> Thanks Makarius, Syntax.parse_term and Syntax.check_term do indeed seem
> to be my friends.
>
> In fact, I sort of wish I'd known about them earlier. I remember in one
> of the record package proofs it was annoying me that I had to construct
> the type
Thanks Makarius, Syntax.parse_term and Syntax.check_term do indeed seem
to be my friends.
In fact, I sort of wish I'd known about them earlier. I remember in one
of the record package proofs it was annoying me that I had to construct
the types explicitly when it felt like I should be able to const
On Mon, 8 Feb 2010, Thomas Sewell wrote:
> Specifically, f is a polymorphic constant, x is a simple function
> application generated by our ML code, and y is supplied by the user and
> must be parsed. So far, our code has simply generated the string
> expression "f (x) (y)" and passed it to Syn
Hello to isabelle-dev.
Suppose some ML code I wrote has terms f, x and y. I'd like to be able
to produce the function application "f x y" with the catch that f, x and
y may all have type parameters that need to be adapted to each other. Is
there any convenient facility for doing this in Isabell
Hi Thomas,
Isabelle internalizes expressions in two steps:
(1) parse :: raw string (type string) -> raw term (type term)
(2) check :: raw term (type term) -> internalized term with types
inferred etc. (type term)
It seems to me that most things you want to do can be done using (2
