From: Nicolas Méric <email@example.com>
let's suppose I have a pseudo term annotation declared as abstract type, and
that I defined a term* command which mimics the term command and adds
the possibility to check the argument passed to the term annotation
as a string. Here is an example:
I'd like to be able to add a markup to have the possibility to be redirected
to the HOL.refl definition when I click on it.
It seems that I need to find a method to compute positions
inside a ML string depicting a term parsed by the parse_term function,
which is called by the read_term function.
Do you have any idea how I can do it?
Or maybe you have another approach to suggest?
Last updated: Dec 05 2021 at 23:19 UTC