Hjalte Sorgenfrei Mac Dalland (Apr 19 2023 at 12:18): Hjalte Sorgenfrei Mac Dalland (Apr 19 2023 at 12:18):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.
Gaëtan Gilbert (Apr 19 2023 at 12:23):Cast (foo, DEFAULTcast, bar) means foo : bar
the other kinds change the : into <: etc
Gaëtan Gilbert (Apr 19 2023 at 12:24):that it says 'constr and '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