Stream: Coq devs & plugin devs

Topic: Constr Cast


view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Apr 19 2023 at 12:23):

Cast (foo, DEFAULTcast, bar) means foo : bar
the other kinds change the : into <: etc

view this post on Zulip 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: Jun 13 2024 at 03:02 UTC