Open
Description
For example:
utop # t1;;
- : term = `\x. s x`
utop # x1, type_of x1;;
- : term * hol_type = (`x`, `:A->bool`)
utop # let s1 = frees t1 |> hd;;
val s1 : term = `s`
utop # instantiate (term_match [] s1 x1) t1;;
- : term = `\x. x x`
The last term is semantically (and type-wise) okay but will not be accepted by the parser (even with explicit type annotations). The reason is that the two xs have different types so the bound variable is not renamed. On the other hand the following sequence produces the correct renaming:
utop # t2;;
- : term = `\x. s + x`
utop # x2, type_of x2;;
- : term * hol_type = (`x`, `:num`)
utop # let s2 = frees t2 |> hd;;
val s2 : term = `s`
utop # instantiate (term_match [] s2 x2) t2;;
- : term = `\x'. x + x'`
M 3558 etadata
Metadata
Assignees
Labels
No labels