Hi, i am trying to figure out how kind_of_term.Cast from constr.mli is supposed to be interpreted.
It has a type of
Cast of 'constr * cast_kind * 'types, but is it casting from the first to the second type or the opposite?
My purpose for asking is that i am developing auto completion for VsCoq where i am calling Constr.kind, and therefore i trying to figure out what useful information i can extract from declarations/goals from Cast.
Cast (foo, DEFAULTcast, bar) means
foo : bar
the other kinds change the
that it says
'types implies that only the rhs is expected to be a type, so it can't be in the other direction
Last updated: Dec 05 2023 at 11:01 UTC