Jason Gross (Oct 25 2022 at 15:44): 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. *)
)
Jason Gross (Oct 25 2022 at 16:02):I guess it's called substn_vars in OCaml
Jason Gross (Oct 25 2022 at 16:07):Ah, I guess it's in LiftSubst.v
Notification Bot (Oct 25 2022 at 16:07):Jason Gross has marked this topic as resolved.
Notification Bot (Oct 25 2022 at 16:08):Jason Gross has marked this topic as unresolved.
Jason Gross (Oct 25 2022 at 16:09):Or, no, hm, it doesn't seem to be there
Jason Gross (Oct 26 2022 at 12:26):(I have written this code myself now, but am still interested if it exists already)
Matthieu Sozeau (Nov 23 2022 at 12:34):Nope, there is basically nothing atm about named variables
Last updated: May 31 2023 at 02:31 UTC