Hi Christian, thanks for the code !
The code was helpful to set my wits to combinators. And it gave another good exercise to distinguish what should be related to contexts and what to theories (formulas of concrete calculations to the former, and predefined patterns like those describing classes of equations to the latter)
On 09/30/2010 07:48 PM, Christian Urban wrote:
Hi Walther, Here my guess what is going on: [...] Even if you use the antiquotation @{term_pat "?l is_polynomial"} (see below) and the assigned type is a schematic type-variable, your way of calculating the substitution does not provide a substitution for types. One solution is to make explicit the type of ?l to avoid any problems with type variables. See below. Hope this is helpful, Christian ------------------------------ theory Test imports Main Complex begin ML {* let val parser = Args.context -- Scan.lift Args.name_source fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt |> ML_Syntax.print_term |> ML_Syntax.atomic in ML_Antiquote.inline "term_pat" (parser >> term_pat) end *} ML {* val t = @{term "a + b * x = (0 ::real)"}; val pat = @{term_pat "?l = (?r ::real)"}; val precond = @{term_pat "is_polynomial (?l::real)"};val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);*} ML {* Envir.subst_term inst precond |> Syntax.string_of_term @{context} |> writeln *} end
_______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
