Stream: MetaCoq

Topic: Free variables?


view this post on Zulip Jason Gross (Oct 25 2022 at 15:44):

Is there an equivalent (in MetaCoq.Template) of Ltac2.Constr.Unsafe.closenl?
(this is

Ltac2 @ external closenl : ident list -> int -> constr -> constr := "ltac2" "constr_closenl".
(** [closenl [x₁;...;xₙ] k c] abstracts over variables [x₁;...;xₙ] and replaces them with
    [Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *)

)

view this post on Zulip Jason Gross (Oct 25 2022 at 16:02):

I guess it's called substn_vars in OCaml

view this post on Zulip Jason Gross (Oct 25 2022 at 16:07):

Ah, I guess it's in LiftSubst.v

view this post on Zulip Notification Bot (Oct 25 2022 at 16:07):

Jason Gross has marked this topic as resolved.

view this post on Zulip Notification Bot (Oct 25 2022 at 16:08):

Jason Gross has marked this topic as unresolved.

view this post on Zulip Jason Gross (Oct 25 2022 at 16:09):

Or, no, hm, it doesn't seem to be there

view this post on Zulip Jason Gross (Oct 26 2022 at 12:26):

(I have written this code myself now, but am still interested if it exists already)

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 12:34):

Nope, there is basically nothing atm about named variables


Last updated: Jan 30 2023 at 17:03 UTC