Re: [isabelle] Better way to beta apply two terms



On Fri, 21 Oct 2011, Steve Wong wrote:

Sorry for digging up a somewhat old post: With Syntax.check_term, can it
sort out the details if the some terms schematic type variables? For example

ML {*
val s = Var (("s",0),dummyT);
val t = Var (("t",0),TVar(("a",0),HOLogic.typeS));
Syntax.check_term @{context} (s$t)
*}

Gives me an error. I know I could use @{cpat ...} but I'm trying to
construct the term without antiquotation.

Depends what you want to do exactly. The following reconstructs types for the given schematic term, treating schematic type variables as fixed in type-inference. The context needs to be configured to allow schematic terms explicitly:

ML {*
val ctxt = @{context} |> Proof_Context.set_mode Proof_Context.mode_schematic;
val s = Var (("s", 0), dummyT);
val t = Var (("t", 0), TVar (("'a", 0), HOLogic.typeS));
Syntax.check_term ctxt (s $ t)
*}

Note that I have used proper type variable name "'a" here. The system does not insist in that, but the behaviour for a TVar called "a" is undefined.

This variant is slightly different, it uses a named type inference parameter that may get instantiated in type-inference:

ML {*
val ctxt = @{context} |> Proof_Context.set_mode Proof_Context.mode_schematic;
val s = Var (("s", 0), dummyT);
val t = Var (("t", 0), Type_Infer.mk_param 0 @{sort HOL.type});
Syntax.check_term ctxt (s $ t)
*}


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.